perm filename BASIS.LIS[BMP,SYS] blob
sn#737797 filedate 1984-01-14 generic text, type T, neo UTF8
;;; -*- Mode: LISP; Package: USER; Base: 10 -*-
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; ;
; Our Theorem Prover ;
; ;
; R. S. Boyer and J Strother Moore ;
; ;
; Austin, Texas ;
; ;
; circa 1983 ;
; ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; LANGUAGES AND MACHINES
; We began working on this code in 1972 in Edinburgh at the Metamathematics
; Unit. The first version was written in POP-2 for an ICL 4130. In Palo
; Alto in 1974 we translated it into Interlisp-10 for a Xerox MAXC and a DEC
; PDP10/BBN-TENEX. We continued developing it at Xerox PARC, SRI, and the
; University of Texas on two DEC-2060s. In 1983, we translated it into
; Maclisp for a DEC-2060 a Honeywell Multics and into Zetalisp for a
; Symbolics 3600.
; OWNERSHIP
; The development of this system has been primarily financed by the National
; Science Foundation and the Office of Naval Research. The NSF Grant Policy
; Manual NSF-77-47, Revised October 1979, states in paragraph 754.2 "Data
; banks and software, produced with the assistance of NSF grants, having
; utility to others in addition to the grantee, shall be made available to
; users, at no cost to the grantee, by publication or, on request, by
; duplication or loan for reproduction by others. ... Any out of pocket
; expenses incurred by the grantee in providing information to third parties
; may be charged to the third party.
; DOCUMENTATION
; The 1978 version of this system was carefully described in "A Computational
; Logic," Academic Press, 1979. But much has changed. (1) An extensive
; amount of "linear" arithmetic has been built-in. (2) We have added the
; notion of metafunctions described in "Metafunctions: Proving Them Correct
; and Using Them Efficiently as New Proof Procedures" in "The Correctness
; Problem in Computer Science," R. S. Boyer and J S. Moore (editors),
; Academic Press, 1981. (3) Equality reasoning in the ground case is
; complete. (4) The mechanism for guessing well-founded relations at
; definition time has been vastly simplified but now requires more explicit
; guidance from the user in the nontrivial cases. (5) A variety of hints can
; be given to the theorem-prover.
; The user's manual for the 1978 version of the theorem-prover is extremely
; out of date. The best we can offer at this time is the file CODE.SUB, "A
; Poor Substitute for a User's Manual for a Theorem Prover for a
; Computational Logic."
; THE SYSTEM
; This code works in Maclisp on a DEC 2060 and on a Honeywell Multics and in
; Zetalisp on a Symbolics 3600. See the file THM.LISP for the Zetalisp
; declaration of the system THM, of which this file, BASIS.LISP, is the first
; module. The file MAKE-SYSTEM.LISP describes how to construct the PDP10
; version. The file start←up.lisp describes how to make the Multics version.
; These Lisps differ, especially on matters related to I/O. The read macros
; #M (for Maclisp), #Q (for Zetalisp), and #+|-(Multics | LISPM | PDP10) are
; used only in the first 1000 lines or so of this file (BASIS.LISP).
; MULTICS MACLISP VS. THE OTHERS
; Perhaps the greatest incompatiblity between Multics Maclisp on the one hand
; and the other Maclisp dialects stems from the fact that on Multics, system
; functions (e.g., CAR, CDR, and CONS) are spelled in lower case (i.e., car,
; cdr, and cons). Some programmers overcome this difference by relying on
; the readtable character translation feature. For example, the code for
; LOOP is written in lower case. It is read on Multics, which does not
; convert from one case to another, in lower case, but when read on a PDP10
; or a LISPM the lower case characters are converted to upper case by
; default. We have taken an opposite approach: on Multics, we have arranged
; it so that READ converts uppercase characters to lower case. This
; arrangement is made in the file start←up.lisp. Read below concerning the
; functions TP-IMPLODE, etc., for the additional complications that the
; different handling of case causes for our theorem prover in Multics. The
; file start←up.lisp also defines DEFMACRO, LOOP, and many other basic
; Maclisp functions that are not in the virgin Multics Maclisp.
; WARNING ABOUT . and #
; Our theorem-prover is implemented as a collection of Lisp programs for
; defining functions (e.g., DEFN) and proving theorems (e.g., PROVE-LEMMA).
; Whoever wishes to use our system must call those functions on Lisp objects.
; In the normal course of events, these Lisp objects are constructed by
; READing characters. For examples, see the the file XXXS.LISP. In
; preparing characters for READ, the diligent user should take care in his
; usage of the consing period and the sharp sign, or he will possibly obtain
; different behavior in Zetalisp than in Maclisp. In Maclisp '(A.B) reads as
; does '(A . B); furthermore, '(A.B.C) produces a "hunk." But in Zetalisp,
; A.B and A.B.C are SYMBOLPs. 2. In Maclisp '(A#/A) reads as does '(A 65).
; But in Zetalisp, A#/A is a SYMBOLP.
; A sufficient precaution is to put spaces on both sides of the consing
; period and to precede each occurrence of # with a space. END OF WARNING.
; QUANTIFIERS
; We are currently expermenting with quantifiers. STATUS FEATURE QUANT
; should be set to get the quantifier version of the system.
#+QUANT
(DEFUN SHARP-OPEN (ARG)
(COND (ARG (AN-ERROR (QUOTE |No digits allowed!|))))
(LET ((TEMP (READ)))
(COND ((NOT (PAIRP TEMP))
(AN-ERROR (QUOTE |Need a list!|)))
((AND (CAR-CDRP (CAR TEMP))
(NOT (ATOM (CDR TEMP)))
(NULL (CDDR TEMP)))
(FIXCAR-CDR TEMP))
((EQ (CAR TEMP) (QUOTE LIST))
(COND ((ATOM (CDR TEMP))
(COND ((NULL (CDR TEMP)) NIL)
(T (AN-ERROR (LIST TEMP (QUOTE |An illegal use of LIST.|))))))
((NULL (CDR (LAST (CDR TEMP))))
(XXXJOIN (QUOTE CONS) (NCONC1 (CDR TEMP) (QUOTE (QUOTE NIL)))))
(T (AN-ERROR (LIST TEMP (QUOTE |An illegal use of LIST.|))))))
((MEMQ (CAR TEMP) (QUOTE (AND OR PLUS TIMES)))
(COND ((< (LENGTH (CDR TEMP)) 2)
(AN-ERROR (LIST TEMP (QUOTE |An illegal use of|) (CAR TEMP))))
((CDR (LAST TEMP))
(AN-ERROR (LIST TEMP (QUOTE |An illegal use of|) (CAR TEMP))))
(T (XXXJOIN (CAR TEMP) (CDR TEMP)))))
(T (AN-ERROR (QUOTE |Need a LIST or CAR-CDRP|))))))
#+QUANT
(#-Multics SETSYNTAX-SHARP-MACRO #+Multics SHARPSIGN-SET-SYNTAX
(QUOTE |(|)
#-LISPM (QUOTE PEEK) #+LISPM (QUOTE :PEEK-MACRO)
(QUOTE SHARP-OPEN))
; LISP PRIMITIVES
; This file, BASIS, has all of the SPECIAL declarations for our
; theorem-prover. We load the compiled version of the file BASIS before we
; compile the rest of the theorem-prover. On both the PDP10 and in Zetalisp,
; the standard definitions of DEFCONST and DEFVAR cause this load to make the
; SPECIAL declarations be in effect for the subsequent compilations. However,
; the standard definitions do not have this effect on Multics; DEFCONST and
; DEFVAR seem merely to generate SETQs in the compiled file. Therefore, on
; Multics, we compile DEFCONST and DEFVAR forms also into PUTPROPs. There
; surely is a better way.
#+Multics
(DEFMACRO DEFCONST (X Y)
`(PROGN (QUOTE COMPILE)
(DECLARE (SPECIAL ,X))
(PUTPROP (QUOTE ,X) T (QUOTE SPECIAL))
(SETQ ,X ,Y)))
#+Multics
(DEFMACRO DEFVAR (X)
`(PROGN (QUOTE COMPILE)
(DECLARE (SPECIAL ,X))
(PUTPROP (QUOTE ,X) T (QUOTE SPECIAL))))
; In Zetalisp, DEFCONSTANT is like DEFCONST except that the value may
; never change and the compiler can use that fact.
#-LISPM
(DEFMACRO DEFCONSTANT (X Y)
`(DEFCONST ,X ,Y))
; Here are the roots of the names of the *.LISP files that comprise the system:
(DEFCONST THEOREM-PROVER-FILES
(QUOTE (BASIS GENFACT EVENTS CODE-1-A CODE-B-D CODE-E-M CODE-N-R CODE-S-Z
IO PPR)))
; LOGNOT and LOGAND are defined in Multics so that that they cannot be nested
; without causing a compiler error. Hence we define:
#+Multics
(DEFMACRO LOGNOT (X) `(BOOLE 6 -1 ,X))
#+Multics
(DEFMACRO LOGAND (X Y) `(BOOLE 1 ,X ,Y))
; ERROR
; In our theorem-prover, error messages are usually printed by the function
; ERROR1, which knows the language of IO1. However, when it is desired
; actually to cause a hard error, we need to call the Lisp function ERROR.
; Unfortunately, on the Lisp machines, ERROR has evolved to become rather
; complex. Below is the simplest invocation of ERROR that we could find that
; didn't cause a compiler warning. The null string below is also the only
; string in the entire theorem-prover.
(DEFUN AN-ERROR (MESSAGE)
#Q (PROGN (PRINT MESSAGE T) (ERROR (QUOTE FERROR) :FORMAT-STRING ""))
#M (ERROR MESSAGE))
; SYMBOLPs
; On the LISPM, the compiler generates warnings that the following functions
; are obsolete: EXPLODEC, EXPLODEN, GETCHAR, GETCHARN, and IMPLODE. Hence
; we define the following "OUR-" macros.
; We never use EXPLODE because it slashes.
(DEFMACRO OUR-EXPLODEC (SYM)
#M `(EXPLODEC ,SYM)
#Q `(LET ((S (STRING ,SYM)))
(LOOP FOR I FROM 0 TO (1- (STRING-LENGTH S))
COLLECT (ASCII (AREF S I)))))
(DEFMACRO OUR-EXPLODEN (SYM)
#M `(EXPLODEN ,SYM)
#Q `(LET ((S (STRING ,SYM)))
(LOOP FOR I FROM 0 TO (1- (STRING-LENGTH S))
COLLECT (AREF S I))))
(DEFMACRO OUR-GETCHAR (SYM N)
#M `(GETCHAR ,SYM ,N)
#Q `(ASCII (AREF (STRING ,SYM) (SUB1 ,N))))
(DEFMACRO OUR-GETCHARN (SYM N)
#M `(GETCHARN ,SYM ,N)
#Q `(AREF (STRING ,SYM) (SUB1 ,N)))
(DEFMACRO OUR-IMPLODE (L)
#M `(IMPLODE ,L)
#Q `(INTERN (APPLY (FUNCTION STRING-APPEND) ,L)))
; On PDP10 and in Zetalisp, literal atoms of the normal variety are
; represented internally by the corresponding Lisp symbols, and terms are
; represented interally with function and variable names that are the
; corresponding Lisp symbols. Thus the term (LESSP (QUOTE A) (QUOTE 3)) is
; represented as (LESSP (QUOTE A) (QUOTE 3)). However, on Multics, the
; representation is (lessp (quote a) (quote 3)). This joke can only be
; carried so far. In particular, in our theory, (UNPACK (QUOTE A)) is equal
; to (CONS (QUOTE 65) 0). Therefore, whenever we look at the interior of
; Lisp symbols, we need to take a different course of action on Multics than
; on other systems.
(DEFMACRO TP-EXPLODEN (SYM)
#-Multics `(OUR-EXPLODEN ,SYM)
#+Multics `(TP-EXPLODEN1 ,SYM))
(DEFMACRO TP-GETCHARN (SYM N)
#-Multics `(OUR-GETCHARN ,SYM ,N)
#+Multics `(TP-GETCHARN1 ,SYM ,N))
(DEFMACRO TP-IMPLODE (L)
#-Multics `(OUR-IMPLODE ,L)
#+Multics `(TP-IMPLODE1 ,L))
; HERALD
; In PDP10 Maclisp, the function HERALD stores the version number of the
; source file of a compiled file under the VERSION property of the root of
; the file name when the compiled file is loaded. In Zetalisp, version
; numbers are kept track of in a separate way by the code that handles
; systems. In Multics, we don't keep track of versions at all.
#Q
(DEFUN HERALD ("E FILE) FILE)
#+Multics
(DEFUN HERALD FEXPR (FILE)
(PRINC (QUOTE |;Loading |) T)
(PRINC (CAR FILE) T)
(TERPRI T))
(HERALD BASIS)
; VARIABLE DECLARATIONS FOR THE OPERATING SYSTEM DEPENDENT CODE
#M
(DEFCONST ALPHABETIC-CASE-AFFECTS-STRING-COMPARISON T)
(DEFCONSTANT EVENT-SEPARATOR-STRING (ASCII #\FORM))
(DEFCONSTANT KEYWORD-BREAK (QUOTE #M BREAK #Q :BREAK))
(DEFCONSTANT KEYWORD-IN (QUOTE #M IN #Q :IN))
(DEFCONSTANT KEYWORD-OUT (QUOTE #M OUT #Q :OUT))
(DEFVAR LIB-FILE)
(DEFVAR LIB-VARS)
(DEFVAR LIB-ATOMS-WITH-PROPS)
(DEFVAR LIB-ATOMS-WITH-DEFS)
(DEFVAR LIB-PROPS)
; LIB-PROPS is automatically set by ADD-SUB-FACT -- when called with INIT arg
; = T -- to be the list, in reverse priority order, of all properties
; declared to be part of the state of the system.
#Q
(DEFCONST LINEL-VALUE 79)
(DEFCONST PROVE-FILE NIL)
; Theorem-prover output is sent to PROVE-FILE. Warnings and error messages
; are also sent to TTY-FILE, if it is different from PROVE-FILE. PROVE-FILE
; and TTY-FILE are initially set to NIL, which means that output goes to the
; default output, which is initially the terminal.
#Q
(DEFCONST STANDARD-RANDSET (SI:RANDOM-CREATE-ARRAY 71. 35. 2.))
; This is an arbitrarily chosen seed for RANDOM used to initialize the random
; number generator for selection of equivalent phrases in output.
; MACROS FOR THE OPERATING SYSTEM DEPENDENT CODE
(DEFMACRO DEFEVENT (NAME ARGS BODY)
; This macro is used to define, in the file EVENTS.LISP, the theorem-prover
; commands. These commands do not evaluate their arguments. Furthermore, to
; permit DEFN and PROVE-LEMMA to have an optional last argument, all of the
; arguments are actually optional, though most of the time a NIL default will
; be rejected by error checking. The decision to have events not evaluate
; their arguments was difficult to make, primarily because it so goes against
; the usual grain of LISP functions. The principal deciding factor was to
; permit a syntax that could be used both to make lists of events to be
; re-executed by REDO-UNDONE-EVENTS and to permit the use of EVAL to execute
; individual events as they were being interactively developed.
#Q
`( DEFUN ,NAME ("E &OPTIONAL ,@ARGS) ,BODY)
#M
`( DEFUN ,NAME FEXPR (ARGLIST)
(LET ,(LOOP FOR ARG IN ARGS AS I FROM 0
COLLECT (LIST ARG `(NTH ,I ARGLIST)))
,BODY)))
(DEFMACRO GET0 (ATM PROP)
#M `(GET00 ,ATM ,PROP)
#Q `(GET ,ATM ,PROP))
(DEFMACRO GET1 (ATM PROP)
#M `(GET11 ,ATM ,PROP)
#Q `(GET ,ATM ,PROP))
#+PDP10
(DEFMACRO NEQ (X Y) `(NOT (EQ ,X ,Y)))
#+(OR Multics LISPM)
(DEFMACRO PAIRP (X) `(NOT (ATOM ,X)))
; We never deal with Maclisp hunks. We check in TRANSLATE that no hunks are
; passed in as terms. Thus the MACLISP definition of PAIRP (i.e., something
; produced by CONS) is consistent with the definition for the LISP machines.
; DEFUNSs FOR THE OPERATING SYSTEM DEPENDENT CODE
(DEFUN ALPHORDER (X Y)
(LET (#Q(ALPHABETIC-CASE-AFFECTS-STRING-COMPARISON T))
(COND ((NUMBERP X)
(COND ((NUMBERP Y) (LESSEQP X Y))
(T T)))
((NUMBERP Y) NIL)
(T (OR (EQ X Y) (ALPHALESSP X Y))))))
#M
(DEFUN CHAR-EQUAL (C1 C2)
(OR (= C1 C2) (AND ALPHABETIC-CASE-AFFECTS-STRING-COMPARISON
(= (IF (OR (< C1 #/a) (> C1 #/z))
C1
(- C1 32))
(IF (OR (< C2 #/a) (> C2 #/z))
C2
(- C2 32))))))
(DEFUN CHAR-IN-STRING (CHAR STRING)
#Q (NOT (NULL (STRING-SEARCH-CHAR CHAR STRING)))
#M (NOT (NULL (MEMBER CHAR (EXPLODEN STRING)))))
#M
(DEFUN CHAR-UPCASE (N)
(COND ((AND (>= N #/a)
(<= N #/z))
(- N 32))
(T N)))
(DEFUN CLOSE? (FILE)
#M (OR (EQ FILE T) (CLOSE FILE))
#Q (PROGN
(COND ((NULL FILE) (SETQ FILE STANDARD-OUTPUT)))
(COND ((EQ FILE T) NIL)
((MEMQ (QUOTE :CLOSE) (SEND FILE (QUOTE :WHICH-OPERATIONS)))
(SEND FILE (QUOTE :CLOSE)))
(T (AN-ERROR (QUOTE |Failure to close a file.|))))))
(DEFUN COMPILE-IF-APPROPRIATE-AND-POSSIBLE (FNS)
; If a function foo is defined in our theory, a function 1foo is defined in
; Lisp. Sometimes during the course of a proof, 1foo may be executed to
; compute the value of foo on certain values. There is a speed benefit to
; compiling 1foo. In Maclisp, the compiler is not in the same Lisp with the
; theorem-prover; in Zetalisp, the compiler is resident. The *.LISP files
; produced by MAKE-LIB may be compiled after loading the compilation of BASIS
; into the compiler. Hence it is possible to obtain the speed of compiled
; functions in the Maclisp version of the theorem-prover, at the expense of
; making a library, running a separate compilation, and using NOTE-LIB to
; load the *.LIB file and the compilation of the .LISP file.
#M FNS
#Q (LOOP FOR FN IN FNS DO
(COND ((NEQ (TYPEP (FSYMEVAL FN))
(QUOTE COMPILED-FUNCTION))
(COMPILE FN)))))
#+PDP10
(DEFUN COPYLIST (L) (LOOP FOR X IN L COLLECT X))
#M
(DEFUN COPYTREE (X)
(IF (ATOM X) X (CONS (COPYTREE (CAR X)) (COPYTREE (CDR X)))))
(DEFUN EXTEND-FILE-NAME (FILE EXTENSION)
; Takes a file name with no extension or version number,
; such as PS:<A>FUM or >udd>proj>fum and produces a file name
; with extension EXTENSION. Thus (EXTEND-FILE-NAME '|PS:<A>FUM| 'LIB)
; yields '|PS:<A>FUM.LIB|. This probably doesn't work right for
; ITS, TOPS-20, or SAIL, but it does for TOPS-20, LISPM, and Multics.
(PACK (LIST FILE (QUOTE /.) EXTENSION)))
(DEFUN FIND-CHAR-IN-FILE (CHAR FILE)
; Assumes that FILE is a stream for a file. Searches for the next occurrence
; of CHAR past current position, if any. If one is found, the file pointer
; is left just after the occurrence and the file pointer is returned.
; Otherwise NIL is returned.
#Q (PROG (ARRAY INDEX COUNT LOC)
(SETQ CHAR (CHARACTER CHAR))
LOOP
(MULTIPLE-VALUE (ARRAY INDEX COUNT)
(SEND FILE (QUOTE :GET-INPUT-BUFFER)))
(COND ((NULL ARRAY) (RETURN NIL)))
(SETQ LOC (%STRING-SEARCH-CHAR CHAR ARRAY INDEX (+ INDEX COUNT)))
(COND (LOC (SEND FILE (QUOTE :ADVANCE-INPUT-BUFFER)
(COND ((< (1+ LOC) (+ INDEX COUNT))
(1+ LOC))
(T NIL)))
(RETURN (SEND FILE (QUOTE :READ-POINTER)))))
(SEND FILE (QUOTE :ADVANCE-INPUT-BUFFER))
(GO LOOP))
#M (LOOP WHILE T WITH CH #+PDP10 AND #+PDP10 ECHOFILES DO
(SETQ CH (TYI FILE -1))
(COND ((= CH -1) (RETURN NIL))
((CHAR-EQUAL CH CHAR) (RETURN (FILEPOS FILE))))))
(DEFUN FIND-STRING-IN-FILE (STRING FILE)
(LET (#+PDP10 ECHOFILES
(STRING-LEN-1 (1- (STRING-LENGTH STRING))))
(IF (EQUAL STRING-LEN-1 -1)
(GETFILEPTR FILE)
(LOOP WITH POS
AND CHARS = (OUR-EXPLODEN STRING)
WITH FIRST-CHAR = (CAR CHARS)
AND OTHER-CHARS = (CDR CHARS)
AND 1+FILE-LEN-STR-LEN = (+ (GETEOFPTR FILE)
(MINUS STRING-LEN-1))
WHILE (SETQ POS (FIND-CHAR-IN-FILE FIRST-CHAR FILE))
DO
(COND ((AND (NOT (> POS 1+FILE-LEN-STR-LEN))
(LOOP FOR CHAR IN OTHER-CHARS ALWAYS
(CHAR-EQUAL CHAR (TYI FILE))))
(RETURN (1- POS)))
(T (SETFILEPTR FILE POS)))))))
(DEFUN FIND-STRING-IN-STRING (PAT STR)
(LOOP FOR TAIL ON (OUR-EXPLODEC STR) AS I FROM (STRING-LENGTH STR) BY -1
WITH PAT-CHARS = (OUR-EXPLODEC PAT) AND PAT-LEN = (STRING-LENGTH PAT)
DO
(COND ((> PAT-LEN I) (RETURN NIL))
((LOOP FOR C IN TAIL AS P IN PAT-CHARS ALWAYS (= C P))
(RETURN (- (STRING-LENGTH STR) I))))))
(DEFUN GET-TOTAL-STATS (DIR)
(LOOP FOR ROOT IN (QUOTE (PROVEALL RSA WILSON GAUSS FORTRAN CONTROLLER PR TMI UNSOLV ZTAK))
WITH STATS
DO (SETQ STATS (SUM-STATS-ALIST
(GET-STATS-FILE
(PACK (LIST DIR ROOT (QUOTE /.) (QUOTE PROOFS))))))
SUM (CAR STATS) INTO TP-TIME
SUM (CADR STATS) INTO IO-TIME
FINALLY (RETURN (LIST TP-TIME IO-TIME))))
#M
(DEFUN GET-FROM-FILE (ATM PROP)
(LOOP FOR TAIL ON (GET-PLIST-FROM-FILE ATM)
BY (QUOTE CDDR)
WHEN (EQ PROP (CAR TAIL))
DO (RETURN (CADR TAIL))))
#M
(DEFUN GET-PLIST-FROM-FILE (ATM)
(LET (#+PDP10 ECHOFILES (LOC (GET ATM (QUOTE LIB-LOC))))
(COND ((NULL LOC) NIL)
((NOT (BOUNDP (QUOTE LIB-FILE))) NIL)
(T (SETFILEPTR LIB-FILE LOC)
(CADR (CADDR (READ LIB-FILE)))))))
(DEFUN GET-STATS-FILE (FILE)
; Returns a list of triplets (event cpu io), where cpu is the number of
; elapsed seconds minus io seconds.
(LET (#+PDP10 ECHOFILES (EVENT-CHAR (OUR-GETCHARN EVENT-SEPARATOR-STRING 1))
(EOF-CONS (CONS NIL NIL)) TEMP TP-TIME IO-TIME)
(SETQ FILE (OPEN FILE KEYWORD-IN))
(SETFILEPTR FILE 0)
(LOOP WHILE (AND (FIND-CHAR-IN-FILE EVENT-CHAR FILE)
(NEQ EOF-CONS (SETQ TEMP (READ FILE EOF-CONS)))
(FIND-CHAR-IN-FILE #/[ FILE)
(NUMBERP (SETQ TP-TIME (READ FILE EOF-CONS)))
(NUMBERP (SETQ IO-TIME (READ FILE EOF-CONS))))
COLLECT (CONS TEMP
(LIST TP-TIME IO-TIME)))))
(DEFUN GET-STATS-OLD-FILE (FILE)
; For use on files with the older ←DEFN(FOO (X) 3) output syntax. Returns a
; list of triplets (event cpu io), where cpu is the number of elapsed seconds
; minus in seconds.
(LET (#+PDP10 ECHOFILES)
(PROGN (SETQ FILE (OPEN FILE KEYWORD-IN))
(SETFILEPTR FILE 0)
(LOOP WHILE (FIND-CHAR-IN-FILE #/← FILE)
COLLECT (CONS (CONS (READ FILE)
(READ FILE))
(AND (FIND-CHAR-IN-FILE #/[ FILE)
(LIST (READ FILE) (READ FILE))))))))
(DEFUN GET-TAIL (ATM PROP)
(LOOP FOR TAIL ON (PLIST ATM) BY (QUOTE CDDR)
WHEN (EQ PROP (CAR TAIL))
DO (RETURN TAIL)))
#M
(DEFUN GET00 (ATM PROP)
(LET ((TEMP (GET-TAIL ATM PROP)))
(COND (TEMP (CADR TEMP))
(T (GET-FROM-FILE ATM PROP)))))
#M
(DEFUN GET11 (ATM PROP)
(LET ((TEMP (GET-TAIL ATM PROP)))
(COND (TEMP (CADR TEMP))
(T (PUT1 ATM (SETQ TEMP (GET-FROM-FILE ATM PROP)) PROP)
TEMP))))
(DEFUN GETEOFPTR (FILE)
#M (LENGTHF FILE)
#Q (SEND FILE (QUOTE :LENGTH)))
(DEFUN GETFILEPTR (FILE)
#M (FILEPOS FILE)
#Q (SEND FILE (QUOTE :READ-POINTER)))
(DEFUN IDATE ()
(POWER-EVAL
#M (APPEND (REVERSE (STATUS DAYTIME)) (REVERSE (STATUS DATE)))
#Q (LOOP FOR I FROM 1 TO 6
AS J IN (MULTIPLE-VALUE-LIST (TIME:GET-TIME))
COLLECT J)
100))
#M
(DEFUN INTERSECTION (X Y)
(LOOP FOR A IN X WHEN (MEMQ A Y) COLLECT A))
(DEFUN KILL-DEFINITION (ATM)
(REMPROP ATM (QUOTE SEXPR))
#M(PROGN (REMPROP ATM (QUOTE SUBR))
(REMPROP ATM (QUOTE EXPR))
(REMPROP ATM (QUOTE LIB-LOC)))
#Q(PROGN (FMAKUNBOUND ATM)
(REMPROP ATM (QUOTE :SOURCE-FILE-NAME))
(REMPROP ATM (QUOTE :PREVIOUS-DEFINITION))))
#+Multics
(DEFUN LENGTHF (FILE)
(LET ((OLD-FILEPOS (FILEPOS FILE)))
(FILEPOS FILE (QUOTE EOF))
; Ridiculous as it seems, in my first experiment with Multics FILEPOS,
; using the 'eof argument as suggested in lisp:manual.doc, the resulting
; filepos seems twice the right answer.
(PROG1 (QUOTIENT (FILEPOS FILE) 2)
(FILEPOS FILE OLD-FILEPOS))))
#Q
(DEFUN LINEL (FILE &OPTIONAL N) FILE
(COND ((FIXP N) (PROG1 LINEL-VALUE (SETQ LINEL-VALUE N)))
(T LINEL-VALUE)))
(DEFUN MAKE-LIB (FILE)
(LET ((BASE 10.) (IBASE 10.) *NOPOINT PRINLEVEL PRINLENGTH
; Do not rudely put carriage returns in the middle of atoms.
#+PDP10 (TERPRI T)
; Do not rudely change the case information of symbols.
#Q (SI:*PRINCASE* (QUOTE :UPCASE))
TEMP PROP-FILE FN-FILE FILE-PLIST
(REVERSED-LIB-PROPS (REVERSE LIB-PROPS)))
#Q FILE-PLIST
(SETQ PROP-FILE (OPEN (EXTEND-FILE-NAME FILE (QUOTE LIB))
KEYWORD-OUT))
(PRINT (LIST (QUOTE INIT-LIB) (KWOTE LIB-PROPS) (KWOTE LIB-VARS))
PROP-FILE)
(LOOP FOR VAR IN LIB-VARS
DO (PRINT (LIST (QUOTE SETQ) VAR (KWOTE (SYMEVAL VAR))) PROP-FILE))
(PRINT (LIST (QUOTE SETQ)
(QUOTE LIB-ATOMS-WITH-PROPS)
(KWOTE LIB-ATOMS-WITH-PROPS))
PROP-FILE)
(PRINT (LIST (QUOTE SETQ)
(QUOTE LIB-ATOMS-WITH-DEFS)
(KWOTE LIB-ATOMS-WITH-DEFS))
PROP-FILE)
(LOOP FOR ATM IN LIB-ATOMS-WITH-PROPS DO
#M (SETQ FILE-PLIST (GET-PLIST-FROM-FILE ATM))
(PRINT (LIST (QUOTE PUT1-LST)
(KWOTE ATM)
(KWOTE
(LOOP FOR PROP IN REVERSED-LIB-PROPS
NCONC
(COND ((SETQ TEMP (GET-TAIL ATM PROP))
(LIST PROP (CADR TEMP)))
#M((LOOP FOR TAIL ON FILE-PLIST
BY (QUOTE CDDR)
WHEN (EQ (CAR TAIL) PROP)
DO
(RETURN
(LIST PROP (CADR TAIL)))))))))
PROP-FILE))
(LOOP FOR ATM IN (REVERSE LIB-ATOMS-WITH-DEFS) DO
(PRINT (LIST (QUOTE PUT1-LST)
(KWOTE ATM)
(KWOTE (LIST (QUOTE SEXPR)
(LIST (QUOTE LAMBDA)
(CADR (SETQ TEMP
(GET0 ATM
(QUOTE SEXPR))))
(CADDR TEMP)))))
PROP-FILE))
(CLOSE PROP-FILE)
(SETQ FN-FILE (OPEN (EXTEND-FILE-NAME FILE (QUOTE LISP))
KEYWORD-OUT))
(LOOP FOR ATM IN (REVERSE LIB-ATOMS-WITH-DEFS) DO
(PRINT (LIST (QUOTE DEFUN)
ATM
(CADR (SETQ TEMP (GET0 ATM (QUOTE SEXPR))))
(CADDR TEMP))
FN-FILE))
(PRINT (LIST (QUOTE COMPILE-IF-APPROPRIATE-AND-POSSIBLE)
(QUOTE LIB-ATOMS-WITH-DEFS))
FN-FILE)
(CLOSE FN-FILE)
#M (LIST PROP-FILE FN-FILE)
#Q (LIST (SEND PROP-FILE (QUOTE :TRUENAME))
(SEND FN-FILE (QUOTE :TRUENAME)))))
(DEFUN NOTE-LIB (FILE1 FILE2)
(COND ((BOUNDP (QUOTE LIB-FILE))
(KILL-LIB)))
#Q (LET ((FS:LOAD-PATHNAME-DEFAULTS FS:LOAD-PATHNAME-DEFAULTS))
(LOAD FILE1)
(SETQ LIB-FILE FILE1))
#M (LET (TEMP
OUTFILES
#+PDP10 (DEFAULTF DEFAULTF)
(NEXT-PTR 0)
(FILE (OPEN FILE1 (QUOTE IN))))
(LOOP UNTIL (EQUAL 0 (SETQ TEMP (READ FILE 0))) DO
(IF (EQ (CAR TEMP) (QUOTE PUT1-LST))
(PUTPROP (CADADR TEMP) NEXT-PTR (QUOTE LIB-LOC))
(EVAL TEMP))
(SETQ NEXT-PTR (GETFILEPTR FILE)))
;; (SETQ LIB-FILE FILE)
;; (OPEN LIB-FILE (QUOTE IN))
(SETQ LIB-FILE (OPEN FILE1 (QUOTE IN)) )
)
(LET ( #Q (FS:LOAD-PATHNAME-DEFAULTS FS:LOAD-PATHNAME-DEFAULTS)
#+PDP10 (DEFAULTF DEFAULTF))
(LOAD FILE2))
LIB-FILE)
(DEFUN OK-SYMBOLP (X)
; From 1974 till 1983 our theorem-prover was implemented in Interlisp-10, in
; which it is the case that, to use Zetalisp terminology, there is only one
; package, every symbolp is interned in it, and symbolp's with the same pname
; are EQ. In the theory in which our system proves theorems, two LITATOMS
; are EQUAL if and only if they have the same UNPACKs. If our theorem-prover
; admitted, say, CHAOS:FOO and USER:FOO as LITATOMS, then it would have to
; conclude that they are EQUAL because their UNPACKs are the same given our
; representation of evgs. However, our theorem-prover also is based upon the
; assumption that two evg's are not EQUAL in the theory if they are not EQUAL
; LISP objects. Therefore, we have to reject some litatoms, such as
; CHAOS:FOO. The rejection occurs in TRANSLATE, where we check that every
; SYMBOLP is OK-SYMBOLP.
; The following definition of OK-SYMBOLP is not sufficient to avoid the
; problems mentioned above if, in MACLISP, OBARRAY does not have its initial
; value, or if someone has mangled the contents of the OBARRAY, or if someone
; has engaged in REMOB's. The following definition is not sufficient to
; avoid the problems in Zetalisp if someone has set PACKAGE to something
; other than USER, has engaged in malicious INTERNing, etc.
#M (EQ X (INTERN X))
#Q (MULTIPLE-VALUE-BIND (SYMBOL INTERNEDP) (INTERN-SOFT X)
(AND INTERNEDP (EQ X SYMBOL))))
(DEFUN OPENP (STREAM)
#M (PROGN STREAM T)
#Q (OR (EQ STREAM TERMINAL-IO)
(MEMQ STREAM (FS:ALL-OPEN-FILES))))
(DEFUN OUR-FBOUNDP (SYM)
#M (GETL SYM
(QUOTE (EXPR FEXPR LEXPR SUBR LSUBR FSUBR MACRO AUTOLOAD ARRAY)))
#Q (FBOUNDP SYM))
(DEFUN PACK (L)
; Takes a list of Lisp SYMBOLPs.
#Q (INTERN (APPLY (FUNCTION STRING-APPEND) L))
#+PDP10 (APPLY (FUNCTION SYMBOLCONC) L)
#+Multics
(IMPLODE (LOOP FOR L1 IN L APPEND (EXPLODEC L1))))
(DEFUN EXPLODE-NUMBER (N)
(COND ((ZEROP N) (LIST (ASCII #/0)))
((< N 0) (CONS (QUOTE -) (EXPLODE-NUMBER (MINUS N))))
(T (NREVERSE (LOOP WHILE (NOT (ZEROP N)) COLLECT
(PROG1 (ASCII (+ #/0 (REMAINDER N 10.)))
(SETQ N (QUOTIENT N 10.))))))))
(DEFUN PREPARE-FOR-THE-NIGHT NIL
#M NIL
#Q (PROGN (GC-ON)
(COND ((MEMQ PROVE-FILE (FS:ALL-OPEN-FILES))
(SEND TERMINAL-IO
(QUOTE :SEND-IF-HANDLES)
(QUOTE :SET-MORE-P)
NIL)))))
(DEFUN PRINT-SYSTEM (FILE)
(PRINC (QUOTE SYSTEM) FILE)
(TERPRI FILE)
(PRINC (QUOTE |[ 0.0 0.0 ]|) FILE)
#M (PROGN
#+PDP10 (LOOP FOR FL IN THEOREM-PROVER-FILES DO
(PRINC FL FILE)
(PRINC (QUOTE |.LISP.|) FILE)
(PRINC (GET FL (QUOTE VERSION)) FILE)
(TERPRI FILE))
(PRINC (QUOTE |Maclisp Version |) FILE)
(PRINC (STATUS LISPVERSION) FILE)
(TERPRI FILE))
#Q (LET ((STANDARD-OUTPUT (OR FILE STANDARD-OUTPUT)))
(PRINT-HERALD)
(DESCRIBE-SYSTEM (QUOTE THM))))
(DEFUN PRINT-DATE-LINE NIL
(PRINT-IDATE (IDATE) PROVE-FILE))
(DEFUN RANDOM-INITIALIZATION (EVENT)
#M(PROGN (RANDOM NIL)
(LOOP FOR I FROM 1 TO (REMAINDER (COUNT EVENT) 11)
DO (RANDOM 10)))
#Q(SI:RANDOM-INITIALIZE STANDARD-RANDSET (COUNT EVENT)))
(DEFUN RANDOM-NUMBER (N)
(RANDOM N #Q STANDARD-RANDSET))
(DEFUN READ-FILE (FILE-NAME)
(LET (#+PDP10 ECHOFILES
(FILE (OPEN FILE-NAME KEYWORD-IN))
(MY-CONS (CONS NIL NIL)))
(LOOP WITH TEMP
WHILE (NEQ MY-CONS
(SETQ TEMP (READ FILE MY-CONS)))
COLLECT TEMP)))
#M
(DEFUN REMQ (I L)
(LOOP FOR X IN L UNLESS (EQ X I) COLLECT X))
#M
(DEFUN REMOVE (I L)
(LOOP FOR X IN L UNLESS (EQUAL X I) COLLECT X))
(DEFUN SETFILEPTR (FILE N)
#Q(SEND FILE (QUOTE :SET-POINTER) N)
#M(FILEPOS FILE N))
(DEFUN STORE-DEFINITION (ATM EXPR)
(PUTPROP ATM EXPR (QUOTE SEXPR))
#Q(PROGN (FSET ATM EXPR) (COMPILE ATM))
; In Maclisp, we copy the definition because it may be executed as an EXPR
; and consequently smashed in macro expansion.
#M(PUTPROP ATM (COPYTREE EXPR) (QUOTE EXPR)))
#M
(DEFUN STRING-DOWNCASE (STR)
(IMPLODE (LOOP FOR N IN (EXPLODEN STR) COLLECT
(COND ((AND (>= N #/A)
(<= N #/Z))
(+ N 32))
(T N)))))
#M
(DEFUN STRING-LENGTH (X)
; Note that MACLISP treats atoms consisting of null (ascii 0) very oldly.
(FLATC X))
(DEFUN R-LOOP ()
(LOOP WHILE T DO
(TERPRI NIL)
(PRINC (QUOTE *) NIL)
(PPR (R (PROG1 (READ NIL) (TERPRI NIL))) NIL)))
(DEFUN TIME-IT (FORM)
(LET ((START-TIME (TIME-IN-60THS)))
(LIST (EVAL FORM) (QUOTIENT (TIME-DIFFERENCE (TIME-IN-60THS) START-TIME)
60.0))))
#M
(DEFUN TIME-DIFFERENCE (X Y)
; The times we give to TIME-DIFFERENCE in MACLISP come from RUNTIME and hence
; do not ever decrease.
(DIFFERENCE X Y))
(DEFUN TIME-IN-60THS ()
; On the 3600, this function returns a number that may wrap around at 2↑31,
; so it's results shouldn't be given to anything but TIME-DIFFERENCE.
#Q (TIME)
; In MACLISP 2130, the following code produces the wrong answer after
; RUNTIME gets to about 10 minutes if we replace 60.0 and 1000000.0 with
; 60. and 1000000. So we use floating point to get things to work.
#M (QUOTIENT (TIMES 60.0 (RUNTIME)) 1000000.0))
#M
(DEFUN UNION (X Y)
(NCONC (LOOP FOR X1 IN X UNLESS (MEMQ X1 Y) COLLECT X1)
Y))
(DEFUN XSEARCH (STRINGS FILE-SPECS)
(IF (ATOM STRINGS) (SETQ STRINGS (LIST STRINGS)))
(IF (ATOM FILE-SPECS) (SETQ FILE-SPECS (LIST FILE-SPECS)))
(LOOP FOR L IN (LOOP FOR FILE-SPEC IN FILE-SPECS
APPEND
#M (LIST (LIST FILE-SPEC))
#Q (FS:DIRECTORY-LIST FILE-SPEC))
WITH NAME AND FILE
WHEN (AND (CAR L)
(PROGN
(TERPRI T)
(SETQ NAME (CAR L))
(PRINC NAME T)
(UNWIND-PROTECT
(PROGN (SETQ FILE (OPEN NAME KEYWORD-IN))
(LOOP FOR STRING IN STRINGS
THEREIS (PROGN
(SETFILEPTR FILE 0)
(FIND-STRING-IN-FILE
STRING FILE))))
(CLOSE? FILE))))
COLLECT
(PROGN (PRINC (QUOTE | Yes.|) T)
#M NAME
#Q (SEND NAME (QUOTE :STRING-FOR-PRINTING)))))
; End of the operating system dependent code.
; VARIABLE DECLARATIONS
(DEFVAR *ALIST*)
(DEFVAR *ARGLIST*)
(DEFVAR *CONTROLLER-COMPLEXITIES*)
(DEFVAR *FILE*)
(DEFVAR *FNNAME*)
(DEFVAR *INDENT*)
(DEFVAR *TYPE-ALIST*)
; Used by REWRITE-FNCALL to store the type-alist so that the lower level
; jumpout can reach up and get it should it need to solidify before jumping.
; The variables 1BTM-OBJECTS, 1F, 1SHELL-QUOTE-MARK, and 1T have
; names that start with 1 because the built-in functions, such as
; 1COUNT, which could be called by some user's function 1FOO, refer
; to these variables.
(DEFVAR 1BTM-OBJECTS)
; This is just a list of all the bottom object function symbols.
(DEFCONSTANT 1F (QUOTE 1FALSE))
; The explicit form of the term (FALSE).
(DEFCONSTANT 1SHELL-QUOTE-MARK (QUOTE 1QUOTE))
; The mark that a constructor expression in an explicit object is represented
; in the CADR.
(DEFCONSTANT 1T (QUOTE 1TRUE))
; The explicit form of the term (TRUE).
(DEFVAR ABBREVIATIONS-USED)
; Used by EXPAND-ABBREVIATIONS and CLAUSIFY-INPUT to record which
; abbreviations were applied.
(DEFVAR ADD-EQUATIONS-TO-DO)
; The second answer returned by ADD-EQUATION consisting of new equations yet
; to be added to the pot.
(DEFCONST ADD-TERM-TO-POT-LST-TEMP (LIST NIL))
; Used by ADD-TERM-TO-POT-LST.
(DEFVAR ALIST)
(DEFVAR ALISTS)
(DEFVAR ALL-FNS-FLG)
(DEFCONST ALL-LEMMAS-USED NIL)
(DEFCONST ALMOST-SUBSUMES-CONSTANT (CONS NIL NIL))
; A special constant used by ALMOST-SUBSUMES. ALMOST-SUBSUMES detects when
; CL1 is almost subsumed by CL2, which means that either CL1 is subsumed by
; CL2 or else it is except for one literal whose negation is in CL2.
; ALMOST-SUBSUMES sets ALMOST-SUBSUMES-LITERAL to this literal. When that
; variable is set to this constant it is interpreted as the message that all
; the literals were subsumed.
(DEFVAR ALMOST-SUBSUMES-LITERAL)
; Used as an extra answer by ALMOST-SUBSUMES.
(DEFCONST ANCESTORS NIL)
; List of the negations of the hypotheses REWRITE is currently trying to
; establish in order to apply lemmas. This list is used by RELIEVE-HYPS and
; RELIEVE-HYPS-NOT-OK to prevent infinite backwards chaining. The list is
; supposed to be bound whenever a new entry is added. Like TYPE-ALIST it is
; a free var only for convenience.
(DEFVAR ANS)
; Used frequently in FOO, FOO1 constructions in which FOO initializes a
; collection site and FOO1 repeatedly adds to it.
(DEFVAR ARGS)
(DEFCONST ARITY-ALIST NIL)
; This is a list associating function names with their arities. Once a
; function has been defined or declared its arity is stored on its property
; list encoded as the length of the CDR of its TYPE-PRESCRIPTION. But it is
; necessary to know the proposed arity of a function even before it has been
; accepted as a legal function and its property list is set up. Thus, this
; list is used, by DEFN0, BOOT-STRAP, and ADD-SHELL0 to declare the arities
; of certain functions during the act of creating them.
(DEFCONST BOOK-SYNTAX-FLG NIL)
; If T this variable causes REDO-UNDONE-EVENTS to print out the events in the
; event list in the syntax used in the "A Computational Logic," rather than
; as LISP forms.
(DEFCONST BOOT-STRAP-INSTRS
(QUOTE ((ADD-SHELL0 FALSE NIL FALSEP NIL)
(ADD-SHELL0 TRUE NIL TRUEP NIL)
(DEFN0 NOT (P)
(IF P (FALSE) (TRUE))
NIL T)
(DEFN0 AND (P Q)
(IF P (IF Q (TRUE) (FALSE)) (FALSE))
NIL T)
(DEFN0 OR (P Q)
(IF P (TRUE) (IF Q (TRUE) (FALSE)))
NIL T)
(DEFN0 IMPLIES (P Q)
(IF P (IF Q (TRUE) (FALSE))
(TRUE))
NIL T)
(ADD-SHELL0 ADD1 ZERO NUMBERP ((SUB1 (ONE-OF NUMBERP) ZERO)))
(DEFN0 LESSP (X Y)
(IF (OR (EQUAL Y 0) (NOT (NUMBERP Y)))
(FALSE)
(IF (OR (EQUAL X 0) (NOT (NUMBERP X)))
(TRUE)
(LESSP (SUB1 X) (SUB1 Y))))
NIL T)
(PUT1 LESSP 0 LEVEL-NO)
(DEFN0 GREATERP (X Y) (LESSP Y X) NIL NIL)
(DEFN0 LEQ (X Y) (NOT (LESSP Y X)) NIL NIL)
(DEFN0 GEQ (X Y) (NOT (LESSP X Y)) NIL NIL)
(DEFN0 LEX2 (L1 L2)
(OR (LESSP (CAR L1) (CAR L2))
(AND (EQUAL (CAR L1) (CAR L2))
(LESSP (CADR L1) (CADR L2))))
NIL NIL)
(DEFN0 LEX3 (L1 L2)
(OR (LESSP (CAR L1) (CAR L2))
(AND (EQUAL (CAR L1) (CAR L2))
(LEX2 (CDR L1) (CDR L2))))
NIL NIL)
(DEFN0 ZEROP (X)
(IF (EQUAL X 0)
T
(IF (NUMBERP X) F T))
NIL T)
(DEFN0 FIX (X)
(IF (NUMBERP X) X 0)
NIL T)
(DEFN0 PLUS (X Y)
(IF (ZEROP X)
(FIX Y)
(ADD1 (PLUS (SUB1 X) Y)))
NIL T)
(ADD-AXIOM1 COUNT-NUMBERP (REWRITE)
(IMPLIES (NUMBERP I)
(EQUAL (COUNT I) I)))
(ADD-AXIOM1 COUNT-NOT-LESSP (REWRITE)
(NOT (LESSP (COUNT I) I)))
(ADD-SHELL0 PACK NIL LITATOM ((UNPACK (NONE-OF) ZERO)))
(ADD-SHELL0 CONS NIL LISTP ((CAR (NONE-OF) ZERO)
(CDR (NONE-OF) ZERO)))
(DEFN0 NLISTP (X)
(NOT (LISTP X))
NIL T)
(ADD-SHELL0 MINUS NIL NEGATIVEP
((NEGATIVE-GUTS (ONE-OF NUMBERP)
ZERO)))
(DEFN0 DIFFERENCE (I J)
(IF (ZEROP I)
0
(IF (ZEROP J)
I
(DIFFERENCE (SUB1 I) (SUB1 J))))
NIL T)
(DEFN0 TIMES (I J)
(IF (ZEROP I)
0
(PLUS J (TIMES (SUB1 I) J)))
NIL T)
(DEFN0 QUOTIENT (I J)
(IF (ZEROP J)
0
(IF (LESSP I J)
0
(ADD1 (QUOTIENT (DIFFERENCE I J) J))))
NIL T)
(DEFN0 REMAINDER (I J)
(IF (ZEROP J)
(FIX I)
(IF (LESSP I J)
(FIX I)
(REMAINDER (DIFFERENCE I J) J)))
NIL T)
(DEFN0 LEGAL-CHAR-CODES NIL
(QUOTE (#/- #/0 #/1 #/2 #/3 #/4 #/5 #/6 #/7 #/8 #/9
#/A #/B #/C #/D #/E #/F #/G #/H #/I #/J #/K #/L #/M
#/N #/O #/P #/Q #/R #/S #/T #/U #/V #/W #/X #/Y #/Z))
NIL NIL)
(DEFN0 ILLEGAL-FIRST-CHAR-CODES NIL
(QUOTE (#/- #/0 #/1 #/2 #/3 #/4 #/5 #/6 #/7 #/8 #/9))
NIL NIL)
(DEFN0 LENGTH (LST)
(IF (LISTP LST)
(ADD1 (LENGTH (CDR LST)))
0)
NIL NIL)
(DEFN0 MEMBER (X LST)
(IF (NLISTP LST)
F
(IF (EQUAL X (CAR LST))
T
(MEMBER X (CDR LST))))
NIL NIL)
(DEFN0 SUBSETP (X Y)
(IF (NLISTP X)
T
(IF (MEMBER (CAR X) Y)
(SUBSETP (CDR X) Y)
F))
NIL NIL)
(DEFN0 LAST (L)
(IF (LISTP L)
(IF (LISTP (CDR L))
(LAST (CDR L))
L)
L)
NIL NIL)
(DEFN0 LEGAL-CHAR-CODE-SEQ (LST)
(AND (LISTP LST)
(SUBSETP LST (LEGAL-CHAR-CODES))
(NOT (MEMBER (CAR LST) (ILLEGAL-FIRST-CHAR-CODES)))
(EQUAL (CDR (LAST LST))
0))
NIL NIL)
(DEFN0 SYMBOLP (X)
(AND (LITATOM X)
(LEGAL-CHAR-CODE-SEQ (UNPACK X)))
NIL NIL)
(DEFN0 LOOKUP (X ALIST)
(IF (NLISTP ALIST)
NIL
(IF (AND (LISTP (CAR ALIST))
(EQUAL X (CAAR ALIST)))
(CDAR ALIST)
(LOOKUP X (CDR ALIST))))
NIL NIL)
(DCL0 ARITY (X))
(DCL0 FORMP (X))
(DEFN0 FORM-LSTP (X)
(IF (NLISTP X)
(EQUAL X NIL)
(AND (FORMP (CAR X))
(FORM-LSTP (CDR X))))
NIL NIL)
(DCL0 APPLY (X LST))
(DCL0 MEANING (X ALIST))
(DEFN0 MEANING-LST (X ALIST)
(IF (NLISTP X)
NIL
(CONS (MEANING (CAR X) ALIST)
(MEANING-LST (CDR X) ALIST)))
NIL NIL)
(SETUP-META-NAMES)
#+QUANT
(DCL APLY (FN ARGS))
#+QUANT
(ADD-FACT APLY LISP-CODE 1APLY)
#+QUANT
(ADD-FACT APLY
LEMMAS
(REWRITE-RULE APLY
NIL
APLY-SIMPLIFIER
NIL))
#+QUANT
(DEFN0 TAME-FORM (TERM)
(IF (EQUAL (CAR TERM) (QUOTE EV))
(AND (LISTP (CADDR TERM))
(EQUAL (CAADDR TERM) (QUOTE QUOTE)))
(IF (EQUAL (CAR TERM) (QUOTE FOR))
(AND (LISTP (CADDDR TERM))
(EQUAL (CAADDDR TERM) (QUOTE QUOTE))
(LISTP (CADDDDDR TERM))
(EQUAL (CAADDDDDR TERM) (QUOTE QUOTE)))
T)) NIL NIL)
#+QUANT
(DEFN0 TAME-TERM (FLG TERM)
(IF (EQUAL FLG (QUOTE LIST))
(IF (NLISTP TERM) T
(AND (TAME-TERM T (CAR TERM))
(TAME-TERM (QUOTE LIST) (CDR TERM))))
(IF (NLISTP TERM) T
(OR (EQUAL (CAR TERM) (QUOTE QUOTE))
(AND (TAME-TERM (QUOTE LIST) (CDR TERM))
(TAME-FORM TERM))))) NIL NIL)
#+QUANT
(DEFN0 EV (FLG FORM ALIST)
(IF (EQUAL FLG (QUOTE LIST))
(IF (NLISTP FORM)
NIL
(CONS (EV T (CAR FORM) ALIST)
(EV FLG (CDR FORM) ALIST)))
(IF (NLISTP FORM)
(IF (LITATOM FORM)
(LOOKUP FORM ALIST)
FORM)
(IF (EQUAL (CAR FORM) (QUOTE QUOTE))
(CADR FORM)
(IF (TAME-FORM FORM)
(APLY (CAR FORM) (EV (QUOTE LIST) (CDR FORM) ALIST))
0)))) NIL NIL)
#+QUANT
(DEFN0 QUANTIFIER-INITIAL-VALUE (FN)
(LOOKUP FN
(QUOTE ((ADD-TO-SET . NIL)
(ALWAYS . 1TRUE)
(APPEND . NIL)
(COLLECT . NIL)
(COUNT . 0)
(DO-RETURN . NIL)
(EXISTS . 1FALSE)
(MAX . 0)
(SUM . 0)
(MULTIPLY . 1)
(UNION . NIL)))) NIL NIL)
#+QUANT
(DEFN0 ADD-TO-SET (X SET) (IF (MEMBER X SET) SET (CONS X SET)) NIL NIL)
#+QUANT
(DEFN0 APPEND (X Y) (IF (LISTP X) (CONS (CAR X) (APPEND (CDR X) Y)) Y) NIL NIL)
#+QUANT
(DEFN0 MAX (X Y) (IF (LESSP X Y) Y X) NIL NIL)
#+QUANT
(DEFN0 UNION (X Y)
(IF (LISTP X)
(IF (MEMBER (CAR X) Y)
(UNION (CDR X) Y)
(CONS (CAR X) (UNION (CDR X) Y)))
Y) NIL NIL)
#+QUANT
(DEFN0 QUANTIFIER-OPERATION (FN ARG REST)
(IF (EQUAL FN (QUOTE ADD-TO-SET))
(ADD-TO-SET ARG REST)
(IF (EQUAL FN (QUOTE ALWAYS))
(AND ARG REST)
(IF (EQUAL FN (QUOTE APPEND))
(APPEND ARG REST)
(IF (EQUAL FN (QUOTE COLLECT))
(CONS ARG REST)
(IF (EQUAL FN (QUOTE COUNT))
(IF ARG (ADD1 REST) REST)
(IF (EQUAL FN (QUOTE DO-RETURN))
ARG
(IF (EQUAL FN (QUOTE EXISTS))
(OR ARG REST)
(IF (EQUAL FN (QUOTE MAX))
(MAX ARG REST)
(IF (EQUAL FN (QUOTE SUM))
(PLUS ARG REST)
(IF (EQUAL FN (QUOTE MULTIPLY))
(TIMES ARG REST)
(IF (EQUAL FN (QUOTE UNION))
(UNION ARG REST)
0))))))))))) NIL NIL)
#+QUANT
(DEFN0 FOR (VAR RANGE CONDITION OP BODY ALIST)
(IF (NLISTP RANGE)
(QUANTIFIER-INITIAL-VALUE OP)
(IF (EV T CONDITION (CONS (CONS VAR (CAR RANGE))
ALIST))
(QUANTIFIER-OPERATION
OP
(EV T BODY (CONS (CONS VAR (CAR RANGE))
ALIST))
(FOR VAR (CDR RANGE) CONDITION OP BODY ALIST))
(FOR VAR (CDR RANGE) CONDITION OP BODY ALIST))) NIL NIL)
(DEFN0 SPLIT (X)
X NIL NIL)
(DEFN0 CHECK (X)
X NIL NIL))))
; This is the list of instructions executed by BOOT-STRAP that initialize the
; theorem prover. A user could not execute this sequence of commands because
; they necessarily violate our new name conventions. For example, axioms
; about SUB1 mention LESSP before LESSP is defined. But LESSP can't be
; defined first because it recurses by SUB1 and before SUB1 were fully
; axiomatized LESSP wouldn't be accepted as a total function. Most of the
; names introduced here are built-into the theorem prover in some sense. For
; example, LESSP is on the list of known well-founded relations, TRUE is
; referenced by name in many routines, the axioms produced by ADD-SHELL use
; IMPLIES and the other logical connectives, as well as LESSP and PLUS, and
; the read-time translation routine uses PACK and CONS to translate QUOTE and
; LIST expressions. However, most of the logical properties of these names
; are made known to the theorem prover in the usual way. For example, TRUE,
; FALSE, and ADD1 are just shells; the logical connectives are just defined
; functions. DIFFERENCE, TIMES, QUOTIENT and REMAINDER are in this list so
; that efficient 1functions can be provided for them.
(DEFCONST BOOT-STRAP-MACRO-FNS (QUOTE (GREATERP LEQ GEQ)))
; Must be a list of function names defined nonrecursively in
; BOOT-STRAP-INSTRS. Expanded away in translate.
(DEFCONST BROKEN-LEMMAS NIL)
(DEFVAR CHRONOLOGY)
; The list of all event names, in reverse chronological order.
(DEFVAR CL2)
(DEFCONST CLAUSE-ALIST NIL)
(DEFVAR COMMONSUBTERMS)
(DEFCONST COMMUTED-EQUALITY-FLG NIL)
(DEFCONST CULPRIT-FUNCTION NIL)
(DEFCONST CURRENT-ATM 0)
; Atom of CURRENT-LIT, set by SIMPLIFY-CLAUSE1 and used by
; ADD-TERM-TO-POT-LST to avoid trying to use linear to add the negation of
; CURRENT-LIT to the pot lst when we know we have already tried it.
(DEFVAR CURRENT-CL)
; The clause whose subterms control which functions get opened up.
(DEFCONST CURRENT-LIT 0)
; During SIMPLIFY-CLAUSE1, CURRENT-LIT is the literal we are currently trying
; to rewrite. ADD-EQUATIONS avoids using any POLY that descends from this
; literal and REWRITE-SOLIDIFY avoids using this literal. Outside of
; SIMPLIFY-CLAUSE1, this variable should not be a term.
(DEFVAR CURRENT-SIMPLIFY-CL)
(DEFVAR CURRENT-TYPE-NO)
; Bound in ADD-SHELL0 for using during the creation of the axioms for a
; shell.
(DEFVAR DECISIONS)
(DEFVAR DEFINITELY-FALSE)
; If FALSE-NONFALSEP returns T then DEFINITELY-FALSE is T if the term is
; equal to FALSE and is NIL if the term is not equal to FALSE.
(DEFVAR DEFN-FLG)
; Used by REWRITE to keep track of whether the current term's value will
; ultimately become either T, F, or -- most importantly -- part of the
; expanded body of a recursive function. If DEFN-FLG is on and the value of
; the term violates REWRITE-FNCALLP, the recursive rewriting of the body can
; be aborted in JUMPOUTP.
(DEFVAR DESCENDANTS)
(DEFVAR DISABLED-LEMMAS)
; This list contains the names of those lemmas that are currently disabled.
; No routine that uses a lemma will consider a lemma whose name is on this
; list.
(DEFVAR DLHDFMLA)
(DEFCONST DO-NOT-USE-INDUCTION-FLG NIL)
; If set to T then PROVE aborts with failure as soon as a clause has to be
; pushed for induction.
(DEFCONST DOTCONS (LIST NIL NIL))
(DEFVAR ELAPSEDTHMTIME)
(DEFCONST ELIM-VARIABLE-NAMES
(QUOTE (X Z V W D C X1 Z1 V1 W1 D1 C1 X2 Z2 V2 W2 D2 C2)))
; This is the list of variables that can be introduced by the elimination of
; destructors -- provided they do not occur in the conjecture being
; generalized. It is important for us to be able to tell how a variable was
; introduced in the theorem. For example, such a question is asked to
; control repeated destructor elimination which might otherwise loop. We use
; the "pretty" variables on this list rather than just GENSYMimg unique names
; because we do not like to see funny variable names in our output. IT IS
; CRUCIAL THAT THIS LIST HAVE NO INTERSECTION WITH GEN-VARIABLE-NAMES -- the
; list used to pick vars for GENERALIZE.
(DEFCONST ELIM-VARIABLE-NAMES1 NIL)
(DEFVAR ENDLIST)
(DEFVAR EVENT-LST)
(DEFCONST EXECUTE-PROCESSES
(QUOTE (SIMPLIFY-CLAUSE SETTLED-DOWN-CLAUSE FERTILIZE-CLAUSE
ELIMINATE-DESTRUCTORS-CLAUSE GENERALIZE-CLAUSE
ELIMINATE-IRRELEVANCE-CLAUSE STORE-SENT)))
; This list is just used by the IO1 function to control such things as to
; whether to indent and print the current goal before printing the process
; specific information.
(DEFCONST EXPAND-LST NIL)
(DEFCONST FAILED-THMS NIL)
; List of all of the conjectures given to PROVE which it failed on during a
; given session with the system. A conjecture is added to the list at setup
; time and taken off only after a successful WRAPUP. Thus the list contains
; conjectures whose attempted proofs were either aborted by the user or
; terminated unsuccessfully by the system. We use the list, together with
; PROVED-THMS, to keep track of what we have done during a session. Note:
; this list is not remembered from one day to another and is reinitialized to
; NIL each time the system is loaded and at the beginning of a PROVEALL.
(DEFVAR FAILURE-ACTION)
(DEFCONST FAILURE-MSG (QUOTE |************** F A I L E D **************|))
; This is the value that is returned by PROVE should a proof fail. It is a
; distinctive message that is guaranteed to catch our eyes if it is ever
; returned as the value of PROVE. Since we often run with the I/O going to a
; file and just the value of PROVE being printed to the terminal, we like for
; failures to be brought to our attention.
(DEFCONST FALSE (QUOTE (QUOTE 1FALSE)))
; This variable is just bound to the internal form of the term (FALSE) for
; convenient coding.
(DEFVAR FALSE-TYPE-ALIST)
(DEFVAR FILE)
(DEFVAR FLATSIZE)
(DEFVAR FMLA)
(DEFVAR FNS)
(DEFVAR FNSTACK)
(DEFCONST FNS-TO-BE-IGNORED-BY-REWRITE NIL)
; Terms beginning with function names on this list are not touched by
; rewrite or expand abbreviations. However, their arguments will have
; already been worked on.
(DEFCONST FORCEIN 38)
#+QUANT
(DEFCONST FOR-OPS
(QUOTE (ADD-TO-SET ALWAYS APPEND COLLECT COUNT
DO-RETURN EXISTS MAX MULTIPLY SUM UNION)))
; These are the quantifier names handled by the FOR function.
(DEFVAR FORM)
(DEFCONST GEN-VARIABLE-NAMES (QUOTE (Y A U B E G H P Q R S)))
; List of variables that can be introduced by generalize. See
; ELIM-VARIABLE-NAMES.
(DEFVAR GEN-VARIABLE-NAMES1)
; Those GEN-VARIABLE-NAMES not occurring in theorem being proved.
(DEFCONST GENERALIZE-LEMMA-NAMES NIL)
(DEFVAR GENERALIZE-LEMMAS)
; The list of GENERALIZE-LEMMA records representing all known GENERALIZE
; lemmas.
(DEFCONST GENERALIZING-SKOS NIL)
(DEFVAR GENRLTLIST)
(DEFCONST HEURISTIC-TYPE-ALIST NIL)
; This type alist is used under ADD-TERMS-TO-POT-LST to determine
; heuristically which terms are numeric and should be linearized. Soundness
; and tail biting are not affected by its setting.
(DEFVAR HIGHER-PROPS)
; The list of properties with higher priority. Used while PUT00 is recursing
; to find out where to put PROP down.
(DEFCONST HINT NIL)
; If nonNIL, then PROVE goes straight into induction.
(DEFVAR HINTS)
; STORE-SENT looks at the HINTS argument of PROVE-LEMMA when deciding whether
; an induction has been done.
(DEFCONST HINT-VARIABLE-ALIST
(QUOTE ((DISABLE TEMPORARILY-DISABLED-LEMMAS NIL NIL)
(EXPAND HINTED-EXPANSIONS T NIL)
(HANDS-OFF FNS-TO-BE-IGNORED-BY-REWRITE NIL NIL)
(NO-BUILT-IN-ARITH NO-BUILT-IN-ARITH-FLG NIL NIL))))
; This is a list of 4-tuples interpreted by APPLY-HINTS. Each element of the
; list is of the form:
; (visible-name internal-variable-name translate-flg default-value).
; Whenever there is a hint whose CAR is one of the visible-names, the
; corresponding internal-variable-name is set by APPLY-HINTS to the CDR of
; the hint. If the translate-flg is T, the CDR of the hint is taken as a
; list of terms and each element of it is TRANSLATEd and the internal
; variable is set to the resulting list. It is assumed that at the top level
; of the system we have arranged -- e.g., by an appropriate DEFVAR -- for
; each of the internal variables to have the value given by the
; default-value. The UNWIND-PROTECT in PROVE-LEMMA, in which hints are
; processed, makes sure the internal variables are restored to their default
; values after the PROVE-LEMMA has terminated. Thus, if a variable is
; DEFVARd to the default value in BASIS and is never set in our code then its
; value is always the default value except when you are executing under a
; PROVE-LEMMA containing a hint with the corresponding visible-name. That
; is, you can regard those variables as having been bound by PROVE-LEMMA to
; the user specified values or to their global default values otherwise.
(DEFCONST HINTED-EXPANSIONS NIL)
; Used to pass information from APPLY-HINTS to SETUP regarding which terms
; the user wants expanded.
(DEFVAR HIST-ENTRY)
(DEFVAR ID-IFF)
(DEFVAR INDENT)
(DEFVAR INDUCTION-CONCL-TERMS)
(DEFCONST INDUCTION-HYP-TERMS NIL)
(DEFVAR INST-HYP)
(DEFCONST IN-ADD-AXIOM-FLG NIL)
(DEFCONST IN-BOOT-STRAP-FLG NIL)
(DEFCONST IN-REDO-UNDONE-EVENTS-FLG NIL)
(DEFCONST IN-PROVE-LEMMA-FLG NIL)
(DEFCONST IO-FN (QUOTE IO1))
; The name of the function called by IO to do the printing during a proof.
; IO is called from several of the theorem proving routines. By redefining
; IO-FN we can alter the amount of IO1 we see. We usually set IO-FN to
; either IO1 or NO-OP.
(DEFCONST IOTHMTIME 0)
; Used to sum up the total amount of time spent in IO during PROVE.
(DEFCONST IPOSITION-ALIST NIL)
(DEFVAR LAST-CLAUSE)
(DEFVAR LAST-EXIT)
; When RELIEVE-HYPS1 fails, the value of LAST-EXIT encodes the reason we
; failed.
(DEFVAR LAST-HYP)
; When RELIEVE-HYPS1 fails, LAST-HYP is set to the HYP that was not relieved.
(DEFVAR LAST-PRIN5-WORD)
(DEFCONST LAST-PRINEVAL-CHAR (QUOTE /.))
; Supposedly this is the last character printed under PRINEVAL, but actually
; it is only accurate when the last character was a punctuation mark.
; Otherwise, it is some arbitrary non-punctuation character.
(DEFVAR LAST-PRINT-CLAUSES)
(DEFCONST LAST-PROCESS NIL)
(DEFVAR LINEARIZE-ASSUMPTIONS-STACK)
(DEFCONST LEFTMARGINCHAR NIL)
; This is the character that IO1 and PPR will print along the left margin of
; the proof tree.
(DEFCONST LEMMA-DISPLAY-FLG NIL)
(DEFCONST LEMMA-TYPES (QUOTE (REWRITE ELIM GENERALIZE META)))
; For each lemma type x there must be a function CHK-ACCEPTABLE-x-LEMMA and
; ADD-x-LEMMA.
(DEFVAR LEMMA-STACK)
(DEFVAR LEMMAS-USED-BY-LINEAR)
; When ADD-TERMS-TO-POT-LST returns CONTRADICTION this list contains the
; names of the lemmas used.
(DEFVAR LINEAR-ASSUMPTIONS)
; When ADD-TERMS-TO-POT-LST returns CONTRADICTION this list contains the
; terms assumed true during the linearization.
(DEFCONST LITATOM-FORM-COUNT-ALIST NIL)
(DEFCONST LITS-THAT-MAY-BE-ASSUMED-FALSE NIL)
; During the construction of the POT-LST in SIMPLIFY-CLAUSE0, we wish to have
; available as hypotheses the negations of the literals in the clause we are
; trying to prove. This variable contains those lits during that
; construction. As lemmas, those lits get stored in POLYs. Then, during
; SIMPLIFY-CLAUSE1's use of linear, we are careful, in ADD-EQUATIONS, not to
; use any POLY that descends from the CURRENT-LIT, by checking that
; CURRENT-LIT is not a MEMBer of the lemmas used to produce the POLY. During
; all calls of REWRITE except those under the construction of the POT-LST in
; SIMPLIFY-CLAUSE0, this variable should be NIL.
(DEFCONST LITS-TO-BE-IGNORED-BY-LINEAR NIL)
; Polys descending from the lits in this list are ignored by the linear
; package.
#+QUANT
(DEFCONSTANT MAGIC-CHAR-NO #/#)
(DEFVAR MAIN-EVENT-NAME)
; All the undo information saved by ADD-FACT is saved on the property list of
; this atom. Thus, one of the main acts of creating an event is to bind this
; name to the event name, so that subsequent ADD-FACTs know who is
; responsible.
(DEFVAR MARG2)
; The PPR variable specifying the righthand margin.
(DEFVAR MASTER-ROOT-NAME)
; Root name for all files created automatically by the theorem prover. The
; function MASTER-ROOT-NAME uses this variable as its value and sets it, when
; NIL, to the user's name.
(DEFVAR MATCH-TEMP)
; Smashed freely in our pattern matcher.
(DEFVAR MATCH-X)
(DEFCONST META-NAMES (QUOTE (APPLY MEANING MEANING-LST ARITY FORMP FORM-LSTP)))
; These are the names that must not appear in definitions and axioms and that
; the MEANING and FORMP simplifiers do not know how to handle.
(DEFVAR MINREM)
(DEFCONST MUST-BE-FALSE NIL)
(DEFCONST MUST-BE-TRUE NIL)
(DEFVAR NAME)
(DEFVAR NAMES)
(DEFVAR NEXT-MEMO-KEY)
(DEFVAR NEXT-MEMO-VAL)
(DEFVAR NEXTIND)
(DEFVAR NEXTNODE)
(DEFCONST NILCONS (CONS NIL NIL))
(DEFCONST NO-BUILT-IN-ARITH-FLG NIL)
; If T the arithmetic package and the storage of arithmetic lemmas is
; disabled.
(DEFVAR NONCONSTRUCTIVE-AXIOM-NAMES)
; The names of all of the axioms added with ADD-AXIOM. We can accept the
; proof of correctness of a metafunction only when this list is empty.
(DEFVAR NUMBER-OF-VARIABLES)
(DEFVAR OBJECTIVE)
(DEFCONST OBVIOUS-RESTRICTIONS NIL)
(DEFVAR ORIG-LEMMA-STACK)
(DEFVAR ORIG-LINEARIZE-ASSUMPTIONS-STACK)
(DEFCONST ORIGEVENT NIL)
(DEFVAR ORIGTHM)
(DEFCONSTANT PARAGRAPH-INDENT 5)
; The number of spaces put out by PRIN5 when it sees the ## token.
(DEFVAR PARENT)
(DEFVAR PARENT-HIST)
(DEFVAR POS)
(DEFCONST PPR-MACRO-LST
(QUOTE (#-QUANT (NOT . CONVERT-NOT) (CONS . CONVERT-CONS)
(CAR . CONVERT-CAR-CDR) (CDR . CONVERT-CAR-CDR)
#+QUANT (FOR . CONVERT-FOR)
#-QUANT (QUOTE . CONVERT-QUOTE))))
; Alist used by PPR to convert terms to their abbreviations for output.
(DEFVAR PPR-MACRO-MEMO)
(DEFVAR PPRFILE)
(DEFCONST PPRFIRSTCOL 35)
(DEFCONST PPRMAXLNS 10000)
(DEFCONST PRINEVAL-FNS
(QUOTE (= AND EQUAL OR NOT EQ EQLENGTH !CLAUSE !CLAUSE-SET !PPR
LENGTH LENGTH-TO-ATOM
!PPR-LIST !LIST PLURALP QUOTE QUOTE PQUOTE CAR CDR
FN-SYMB FFN-SYMB ARGN FARGN ARGS FARGS QUOTEP FQUOTEP)))
; This is the list of LISP functions that PRINEVAL -- actually PEVAL -- can
; evaluate. To add a function to the list you must make sure that the
; function mentions no specvars other than those already declared, and that
; the function is essentially a LAMBDA -- rather than an NLAMBDA -- in that
; all of its args get evald.
(DEFVAR PROCESS)
(DEFVAR PROCESS-CLAUSES)
(DEFVAR PROCESS-HIST)
(DEFVAR PROP)
(DEFVAR PROPLIST)
(DEFVAR PROVE-TERMINATION-LEMMAS-USED)
(DEFCONST PROVED-THMS NIL)
; List of all theorems proved during a given session. See FAILED-THMS.
(DEFCONST R-ALIST NIL)
(DEFVAR RECOGNIZER-ALIST)
; An alist that associates with each shell recognizer, e.g., NUMBERP, the
; type set recognized by that predicate, e.g., the bit mask representing the
; set whose only element is the type class for NUMBERs. Obviously, the list
; is used to help determine if recognizer expressions can be simplified to
; TRUE (when the type set of the argument is the type set recognized) or
; FALSE (when the type set of the argument does not intersect with the one
; recognized).
(DEFVAR RECORD-DECLARATIONS)
(DEFVAR RECORD-TEMP)
; Smashed repeatedly during our record package manipulations.
(DEFVAR RELIEVE-HYPS-NOT-OK-ANS)
(DEFVAR REMAINDER)
(DEFVAR SCRIBE-FLG)
(DEFVAR SETQ-LST)
(DEFVAR SHELL-ALIST)
; An alist associating each shell name, e.g., CONS, with its type number.
; The type set of the shell -- that is, the set containing only that type of
; object -- is just the bit mask with one 1 in it, at the bit whose position
; is the class's type no. Thus, the type number for FALSE is 0, TRUE 1, etc.
; The alist is used when determining the type of an expression beginning with
; the shell name.
(DEFVAR SHELL-POCKETS)
; A list of pockets consisting of a shell name and the list of its
; destructors, with the shell name in the car.
(DEFVAR SIMPLIFY-CLAUSE-MAXIMALLY-CLAUSES)
(DEFVAR SIMPLIFY-CLAUSE-MAXIMALLY-HIST)
(DEFVAR SIMPLIFY-CLAUSE-POT-LST)
; The ADD-EQUATIONS-WITH-LEMMAS of the top-level clause in SIMPLIFY-CLAUSE.
(DEFVAR SINGLETON-TYPE-SETS)
; A list of type sets of shells with no components. If a shell has no
; components then an expression beginning with the shell name represents a
; unique constant, e.g., (TRUE) or (FALSE) or other shells the user might
; introduce such as (ERROR). If an expression is known to have as its type
; set one of the singleton type sets, the expression is known to be equal to
; the corresponding object.
(DEFVAR SPACELEFT)
(DEFCONST STACK NIL)
(DEFVAR STARTLIST)
(DEFCONSTANT STRING-ONE (QUOTE |1|))
(DEFVAR T2)
(DEFCONST TAB-SIZE 8.)
(DEFVAR TEMP-TEMP)
; Used freely by anyone, but liable to be set by a call of any function.
(DEFVAR TEMP1)
(DEFCONST TEMPORARILY-DISABLED-LEMMAS NIL)
(DEFCONST TERMS-TO-BE-IGNORED-BY-REWRITE NIL)
(DEFVAR TEST-LST)
(DEFVAR THM)
(DEFCONST TRANSLATE-TO-LISP-TIME 0)
; Incremented by TRANSLATE-TO-LISP to record the amount of time spent in
; optimizing user defined functions.
(DEFCONSTANT TREE-INDENT 2)
; The number of spaces IO1 indents when printing out the tree structure of
; the proof.
(DEFCONSTANT TREE-LINES 2)
; The number of lines IO1 skips between each node of the tree structure in a
; proof.
(DEFCONST TRUE (QUOTE (QUOTE 1TRUE)))
; A variable bound to internal form of the term (TRUE) to make coding more
; convenient.
(DEFCONST TRUE-CLAUSE (LIST TRUE))
; The clause whose only literal is the (TRUE) literal. This just makes
; coding more convenient.
(DEFCONST TRUE-TYPE-ALIST NIL)
(DEFCONST TTY-FILE NIL)
; The name of the file to which error and warning messages will be printed.
(DEFCONST TYPE-ALIST NIL)
; An alist used by TYPE-SET -- and hence almost every routine in the theorem
; prover -- to associate with a term its type bits. The list is always
; protected by rebinding it when a new entry must be added. However it has
; become a GLOBAL free var out of convenience. TYPE-SET cannot be trusted
; unless TYPE-ALIST is accurately set.
(DEFCONSTANT TYPE-SET-BOOLEAN 3)
; The bit pattern representing the set containing only the type classes TRUE
; and FALSE.
(DEFCONSTANT TYPE-SET-CONS 16)
; Type set of CONS exprs.
(DEFCONSTANT TYPE-SET-FALSE 1)
; The bit pattern representing the set containing only the type class FALSE.
(DEFCONSTANT TYPE-SET-LITATOMS 8)
; Type set of PACK exprs.
(DEFCONSTANT TYPE-SET-NEGATIVES 32)
; Type set of MINUS exprs.
(DEFCONSTANT TYPE-SET-NUMBERS 4)
; The bit pattern representing the set containing only the type class of 0
; and ADD1 -- i.e., that set recognized by NUMBERP.
(DEFVAR TYPE-SET-TERM1)
(DEFCONSTANT TYPE-SET-TRUE 2)
; The bit pattern representing the set containing only the type class TRUE.
(DEFCONSTANT TYPE-SET-UNKNOWN -1)
; The bit pattern representing the set of all type classes.
(DEFCONST UN-PRODUCTIVE-PROCESSES
(QUOTE (SETTLED-DOWN-CLAUSE STORE-SENT POP SUBSUMED-ABOVE
SUBSUMED-BY-PARENT SUBSUMED-BELOW
FINISHED)))
; Used by IO1 to determine if the descendants list of the current process
; should be printed out. Some processes, such as simplification, lead to n
; new clauses, where n=0 means the parent was proved. For unproductive
; processes, such as SETUP, the list of descendants is meaningless since the
; process does not change the current goal -- as far as the IO is concerned.
(DEFCONST UNDONE-BATCH-COMMANDS NIL)
(DEFVAR UNDONE-EVENTS)
(DEFCONST UNDONE-EVENTS-STACK NIL)
(DEFVAR UNIFY-SUBST)
(DEFVAR UNIVERSE)
(DEFCONST USE-NO-LEMMAS-FLG NIL)
; When non-NIL this flag prevents REWRITE from using rewrite lemmas, axioms,
; and recursive definitions. It is still free to use built in information
; (e.g., about EQUAL) and the type set information through
; TYPE-PRESCRIPTIONs, RECOGNIZER-ALIST, etc. The option is used when PROVE
; is first given a theorem and we want to eliminate the propositional
; calculus stuff in it -- expanding the IMPLIES and NOTs etc -- without
; wasting time trying to rewrite the interior recursive part of the theorem
; until we have dug out all the hypotheses and put the thing into clausal
; form.
(DEFVAR VAL)
(DEFVAR VAR-ALIST)
(DEFCONST WELL-ORDERING-RELATIONS (QUOTE (LESSP LEX2 LEX3)))
; This is the list of all known well-founded relations -- the name is
; misleading. A function gets to be on this list by an act of god -- i.e.,
; the user -- since the theorem prover cannot prove that a relation is
; well-founded.
(DEFCONST ZERO (QUOTE (QUOTE 0)))
; Internal representation of (ZERO).
(DEFMACRO 1IF (X Y Z) `(COND ((EQ ,X 1F) ,Z) (T ,Y)))
(DEFMACRO ADD-SUB-FACT-BODY X (GENERATE-ADD-SUB-FACT1 X))
(DEFMACRO ACCESS X (ACCESS-MACRO (CAR X) (CADR X) (CADDR X)))
(DEFMACRO ARGN TAIL (ARGN-MACRO TAIL))
(DEFMACRO BINDINGS TAIL (BINDINGS-MACRO TAIL))
(DEFMACRO CHANGE X (CHANGE-MACRO (CAR X) (CADR X) (CADDR X) (CADDDR X)))
(DEFMACRO DISABLEDP (NAME) `(OR (MEMQ (SETQ TEMP-TEMP ,NAME)
TEMPORARILY-DISABLED-LEMMAS)
(CDDR (ASSQ TEMP-TEMP DISABLED-LEMMAS))))
(DEFMACRO FARGN TAIL (FARGN-MACRO TAIL))
(DEFMACRO FARGS (X) `(CDR ,X))
(DEFMACRO FCONS-TERM TAIL (CONS (QUOTE CONS) TAIL))
(DEFMACRO FCONS-TERM* TAIL (CONS (QUOTE LIST) TAIL))
(DEFMACRO FFN-SYMB (X) `(CAR ,X))
(DEFMACRO FN-SYMB TAIL (FN-SYMB-MACRO TAIL))
(DEFMACRO FQUOTEP (X) `(EQ (CAR ,X) (QUOTE QUOTE)))
(DEFMACRO LOGBIT (N) `(LSH 1 ,N))
(DEFMACRO LOGDIFF (X Y) `(BOOLE 4 ,X ,Y))
(DEFMACRO MAKE X (MAKE-MACRO (CAR X) (CDR X)))
(DEFMACRO MATCH X (MATCH-MACRO (CAR X) (CADR X)))
(DEFMACRO MATCH! X (MATCH!-MACRO (CAR X) (CADR X)))
(DEFMACRO NVARIABLEP (X) `(PAIRP ,X))
(DEFMACRO PQUOTE (X) `(QUOTE ,X))
(DEFMACRO PRIND (X FILE)
`(LET ((TEMP ,X))
(PRINC TEMP ,FILE)
(SETQ POS (+ POS
(COND ((SYMBOLP TEMP) (STRING-LENGTH TEMP))
(T (FLATC TEMP)))))))
(DEFMACRO QUOTEP (X) `(AND (PAIRP (SETQ TEMP-TEMP ,X))
(EQ (CAR TEMP-TEMP) (QUOTE QUOTE))))
(DEFMACRO SWAP (X Y) `(SETQ ,X (PROG1 ,Y (SETQ ,Y ,X))))
(DEFMACRO TYO1 (X FILE) `(PROGN (TYO ,X ,FILE)
(SETQ POS (1+ POS))))
(DEFMACRO TYPE-PRESCRIPTION (X)
`(CDAR (GET1 ,X (QUOTE TYPE-PRESCRIPTION-LST))))
(DEFMACRO VALUEP (X) `(QUOTEP ,X))
(DEFMACRO VARIABLEP (X) `(ATOM ,X))
(DEFUN 1CAR (X1)
(COND ((ATOM X1) 0)
((EQ (CAR X1) (QUOTE 1QUOTE)) 0)
(T (CAR X1))))
(DEFUN 1CDR (X1)
(COND ((ATOM X1) 0)
((EQ (CAR X1) (QUOTE 1QUOTE)) 0)
(T (CDR X1))))
(DEFUN ACCESS-MACRO (RECORD-NAME FIELD RECORD)
(COND ((CADDR (ASSQ RECORD-NAME RECORD-DECLARATIONS))
(LIST (QUOTE CAR)
(CELL (GET-FIELD-NUMBER RECORD-NAME FIELD)
RECORD)))
(T (LIST (QUOTE COND)
(LIST (LIST (QUOTE AND)
(LIST (QUOTE PAIRP)
(COND ((PAIRP RECORD)
(LIST (QUOTE SETQ)
(QUOTE RECORD-TEMP)
RECORD))
(T RECORD)))
(LIST (QUOTE EQ)
(LIST (QUOTE CAR)
(COND ((PAIRP RECORD)
(QUOTE RECORD-TEMP))
(T RECORD)))
(KWOTE RECORD-NAME)))
(LIST (QUOTE CAR)
(CELL (GET-FIELD-NUMBER RECORD-NAME FIELD)
(COND ((PAIRP RECORD)
(QUOTE RECORD-TEMP))
(T RECORD)))))
(LIST T (LIST (QUOTE ACCESS-ERROR)
(KWOTE RECORD-NAME)))))))
(DEFUN ADD-TO-SET (X Y)
(COND ((MEMBER X Y) Y)
(T (CONS X Y))))
(DEFUN ARGN-MACRO (TAIL)
(COND ((FIXP (CADR TAIL))
(SUB-PAIR (QUOTE (TERM CELL N))
(LIST (CAR TAIL)
(CELL (CADR TAIL) (QUOTE TEMP-TEMP))
(CADR TAIL))
(QUOTE (COND ((NEQ (CAR (SETQ TEMP-TEMP TERM))
(QUOTE QUOTE))
(CAR CELL))
(T (ARGN0 TEMP-TEMP N))))))
(T (CONS (QUOTE ARGN0)
TAIL))))
(DEFUN BINDINGS-MACRO (TAIL)
(IF (ATOM TAIL)
NIL
`(CONS (CONS ,(CAR TAIL) ,(CADR TAIL))
,(BINDINGS-MACRO (CDDR TAIL)))))
(DEFUN CELL (N FIELD)
(COND ((= N 0) FIELD)
(T (LIST (QUOTE CDR)
(CELL (1- N) FIELD)))))
(DEFUN CREATE-LEMMA-STACK (N)
(SETQ ORIG-LEMMA-STACK (SETQ LEMMA-STACK (CREATE-STACK1 N)))
(RPLACA LEMMA-STACK (QUOTE TOP))
NIL)
(DEFUN CREATE-LINEARIZE-ASSUMPTIONS-STACK (N)
(SETQ ORIG-LINEARIZE-ASSUMPTIONS-STACK
(SETQ LINEARIZE-ASSUMPTIONS-STACK (CREATE-STACK1 N)))
(RPLACA LINEARIZE-ASSUMPTIONS-STACK (QUOTE TOP))
NIL)
(DEFUN CREATE-STACK1 (N)
(LET (STK)
(SETQ STK (LOOP FOR I FROM 1 TO (* 2 N) COLLECT NIL))
(LOOP FOR TAIL ON STK BY (QUOTE CDDR) UNTIL (NULL (CDDR TAIL))
DO (RPLACA (CDDDR TAIL)
TAIL))
STK))
(DEFUN EQLENGTH (X N) (EQUAL N (LENGTH X)))
(DEFUN FARGN-MACRO (TAIL)
(COND ((FIXP (CADR TAIL))
(LIST (QUOTE CAR)
(CELL (CADR TAIL)
(CAR TAIL))))
(T (LIST (QUOTE NTH)
(CADR TAIL)
(CAR TAIL)))))
(DEFUN FN-SYMB-MACRO (TAIL)
(SUBST (CAR TAIL)
(QUOTE TERM)
(QUOTE (COND ((NEQ (QUOTE QUOTE) (CAR (SETQ TEMP-TEMP TERM)))
(CAR TEMP-TEMP))
(T (FN-SYMB0 (CADR TEMP-TEMP)))))))
(DEFUN GET-FIELD-NUMBER (RECORD-NAME LITATOM)
(SETQ TEMP-TEMP (ASSQ RECORD-NAME RECORD-DECLARATIONS))
(COND ((LOOP FOR I FROM (COND ((CADDR TEMP-TEMP) 0)
(T 1))
AS FIELD IN (CADR TEMP-TEMP) WHEN (EQ FIELD LITATOM)
DO (RETURN I)))
(T (TERPRI T)
(PRINC
(QUOTE |***** Undeclared record name or illegal field name *****|)
T)
(TERPRI T)
(SPACES 6 T)
(PRIN1 (LIST RECORD-NAME LITATOM) T)
(ITERPRI T)
1)))
(DEFUN IPOSITION (FILE N FLG)
(LET (PAIR)
(COND ((NULL (SETQ PAIR (ASSQ FILE IPOSITION-ALIST)))
(SETQ IPOSITION-ALIST
(CONS (SETQ PAIR (CONS FILE 0)) IPOSITION-ALIST))))
(COND ((NULL N) (CDR PAIR))
(FLG (PROG1 (CDR PAIR) (RPLACD PAIR (+ N (CDR PAIR)))))
(T (PROG1 (CDR PAIR) (RPLACD PAIR N))))))
(DEFUN ITERPRI (FILE)
(IPOSITION FILE 0 NIL)
(TERPRI FILE))
(DEFUN ITERPRIN (N FILE)
(LOOP FOR I FROM 1 TO N DO (ITERPRI FILE)))
(DEFUN ITERPRISPACES (N FILE)
(ITERPRI FILE)
(TABULATE N FILE))
(DEFUN IPRIN1 (X FILE)
(IPOSITION FILE (FLATSIZE X) T)
(PRIN1 X FILE))
(DEFUN IPRINC (X FILE)
(IPOSITION FILE
(COND ((SYMBOLP X)
(STRING-LENGTH X))
(T (FLATC X)))
T)
(PRINC X FILE))
(DEFUN IPRINT (X FILE)
(IPOSITION FILE (FLATSIZE X) NIL)
(PRINT X FILE))
(DEFUN ISPACES (N FILE)
(COND ((<= N 0) NIL)
(T (IPOSITION FILE N T)
(LOOP FOR I FROM 1 TO N DO (TYO #\SPACE FILE)))))
(DEFUN KWOTE (X) `(QUOTE ,X))
(DEFUN MAKE-MACRO (RECORD ARGLIST)
(COND ((NOT (SETQ TEMP-TEMP (ASSQ RECORD RECORD-DECLARATIONS)))
(ITERPRI T)
(IPRINC
(QUOTE |***** Undeclared record name in MAKE expression *****|)
T)
(ITERPRI T)
(SPACES 6 T) (PRIN1 RECORD T) (TERPRI T)
NIL)
((= (LENGTH ARGLIST) (LENGTH (CADR TEMP-TEMP)))
(COND ((CADDR TEMP-TEMP)
(CONS (QUOTE LIST) ARGLIST))
(T (CONS (QUOTE LIST)
(CONS (KWOTE RECORD) ARGLIST)))))
(T (IPRINC (QUOTE |***** Wrong number of args *****|) T)
(TERPRI T)
(SPACES 6 T)
(PRIN1 (CONS (QUOTE MAKE) (CONS RECORD ARGLIST)) T)
(ITERPRI T)
NIL)))
(DEFUN MATCH-MACRO (TERM PAT)
(COND ((PAIRP TERM)
(LIST (QUOTE PROGN)
(LIST (QUOTE SETQ) (QUOTE MATCH-TEMP) TERM)
(MATCH1-MACRO (QUOTE MATCH-TEMP) PAT)))
(T (MATCH1-MACRO TERM PAT))))
(DEFUN MATCH!-MACRO (TERM PAT)
(LIST (QUOTE OR)
(MATCH-MACRO TERM PAT)
(QUOTE (AN-ERROR (QUOTE |MATCH! failed!|)))))
(DEFUN MATCH1-MACRO (TERM PAT)
(LET (TEST-LST SETQ-LST)
(MATCH2-MACRO TERM PAT)
(LIST (QUOTE COND)
(CONS
(COND ((NULL TEST-LST) T)
((NULL (CDR TEST-LST)) (CAR TEST-LST))
(T (CONS (QUOTE AND) TEST-LST)))
(NCONC1 SETQ-LST T)))))
(DEFUN MATCH2-MACRO (TERM PAT)
(COND ((ATOM PAT)
(COND ((EQ PAT (QUOTE &)) NIL)
((OR (EQ PAT T) (EQ PAT NIL))
(PRINC (QUOTE |***** Attempt to smash T or NIL ignored *****|)
T)
(TERPRI T)
(SPACES 6 T)
(PRIN1 (CONS (QUOTE MATCH) MATCH-X) T)
(ITERPRI T))
((SYMBOLP PAT)
(SETQ SETQ-LST (NCONC1 SETQ-LST (LIST (QUOTE SETQ) PAT TERM))))
(T (SETQ TEST-LST
(NCONC1 TEST-LST (LIST (QUOTE EQUAL) PAT TERM))))))
((EQ (QUOTE CONS) (CAR PAT))
(SETQ TEST-LST (NCONC1 TEST-LST (LIST (QUOTE PAIRP) TERM)))
(MATCH2-MACRO (LIST (QUOTE CAR) TERM) (CADR PAT))
(MATCH2-MACRO (LIST (QUOTE CDR) TERM) (CADDR PAT)))
((EQ (QUOTE QUOTE) (CAR PAT))
(COND ((SYMBOLP (CADR PAT))
(SETQ TEST-LST
(NCONC1 TEST-LST
(LIST (QUOTE EQ)
(LIST (QUOTE QUOTE) (CADR PAT))
TERM))))
(T (SETQ TEST-LST (NCONC1 TEST-LST
(LIST (QUOTE EQUAL)
(LIST (QUOTE QUOTE)
(CADR PAT))
TERM))))))
(T (COND ((NEQ (CAR PAT)
(QUOTE LIST))
(SETQ PAT (CONS (QUOTE LIST)
(CONS (LIST (QUOTE QUOTE)
(CAR PAT))
(CDR PAT))))))
(LOOP FOR SUBPAT IN (CDR PAT) DO (SETQ TEST-LST
(NCONC1 TEST-LST
(LIST (QUOTE PAIRP)
TERM)))
(MATCH2-MACRO (LIST (QUOTE CAR)
TERM)
SUBPAT)
(SETQ TERM (LIST (QUOTE CDR)
TERM)))
(SETQ TEST-LST (NCONC1 TEST-LST (LIST (QUOTE EQ)
TERM NIL))))))
(DEFUN NCONC1 (X Y) (NCONC X (LIST Y)))
(DEFUN RECORD-DECLARATION (RECORD-NAME FIELD-LST CHEAP)
(LET (LST)
(COND ((NOT (BOUNDP (QUOTE RECORD-DECLARATIONS)))
(SETQ RECORD-DECLARATIONS NIL)))
(COND ((NOT (OR (PAIRP FIELD-LST) (EQ FIELD-LST NIL)))
(AN-ERROR (LIST (QUOTE |Illegal field list: |) FIELD-LST)))
((NOT (OR (EQ CHEAP T) (EQ CHEAP NIL)))
(AN-ERROR (LIST (QUOTE |Illegal cheap flag: |) CHEAP))))
(SETQ LST (LIST RECORD-NAME (COPYTREE FIELD-LST) CHEAP))
(COND ((MEMBER LST RECORD-DECLARATIONS) NIL)
((ASSQ (CAR LST) RECORD-DECLARATIONS)
(SETQ RECORD-DECLARATIONS
(CONS LST (REMOVE (ASSQ (CAR LST) RECORD-DECLARATIONS)
RECORD-DECLARATIONS)))
(IPRINC (CAR LST) T)
(IPRINC (QUOTE | redefined.|) T)
(ITERPRI T))
(T (SETQ RECORD-DECLARATIONS
(CONS LST RECORD-DECLARATIONS))))
RECORD-NAME))
(DEFUN RECORD-DECLARATION-LST (X)
(LOOP FOR TUPLE IN X DO (APPLY (FUNCTION RECORD-DECLARATION) TUPLE)))
(DEFUN SPACES (N FILE)
(COND ((<= N 0) NIL)
(T (LOOP FOR I FROM 1 TO N DO (TYO #\SPACE FILE)))))
(DEFUN SPELL-NUMBER (N)
(SELECTQ N
(0 (QUOTE |zero|))
(1 (QUOTE |one|))
(2 (QUOTE |two|))
(3 (QUOTE |three|))
(4 (QUOTE |four|))
(5 (QUOTE |five|))
(6 (QUOTE |six|))
(7 (QUOTE |seven|))
(8 (QUOTE |eight|))
(9 (QUOTE |nine|))
(10 (QUOTE |ten|))
(OTHERWISE
N)))
(DEFUN CHANGE-MACRO (RECORD-NAME FIELD RECORD VALUE)
(COND ((CADDR (ASSQ RECORD-NAME RECORD-DECLARATIONS))
(LIST (QUOTE RPLACA)
(CELL (GET-FIELD-NUMBER RECORD-NAME FIELD) RECORD)
VALUE))
(T (LIST (QUOTE COND)
(LIST (LIST (QUOTE AND)
(LIST (QUOTE PAIRP)
(COND ((PAIRP RECORD)
(LIST (QUOTE SETQ)
(QUOTE RECORD-TEMP)
RECORD))
(T RECORD)))
(LIST (QUOTE EQ)
(LIST (QUOTE CAR)
(COND ((PAIRP RECORD)
(QUOTE RECORD-TEMP))
(T RECORD)))
(KWOTE RECORD-NAME)))
(LIST (QUOTE RPLACA)
(CELL (GET-FIELD-NUMBER RECORD-NAME FIELD)
(COND ((PAIRP RECORD)
(QUOTE RECORD-TEMP))
(T RECORD)))
VALUE))
(LIST T (LIST (QUOTE ACCESS-ERROR)
(KWOTE RECORD-NAME)))))))
(DEFUN SUB-PAIR (L1 L2 X)
(COND ((LOOP FOR Z IN L2 AS Y IN L1 WHEN (EQUAL Y X)
THEREIS (PROGN (SETQ TEMP-TEMP Z) T))
TEMP-TEMP)
((ATOM X) X)
(T (CONS (SUB-PAIR L1 L2 (CAR X)) (SUB-PAIR L1 L2 (CDR X))))))
(RECORD-DECLARATION-LST
(QUOTE
((CANDIDATE (SCORE CONTROLLERS CHANGED-VARS UNCHANGEABLE-VARS
TESTS-AND-ALISTS-LST JUSTIFICATION INDUCTION-TERM
OTHER-TERMS)
NIL)
; This record is used to represent one of the plausible inductions that must
; be considered. The SCORE represents some fairly artificial estimation of
; how many terms in the conjecture want this induction. CONTROLLERS is the
; list of the controllers -- including unchanging controllers -- for all the
; inductions merged to form this one. The CHANGED-VARS is a list of all
; those variables that will be instantiated (non-identically) in some
; induction hypotheses. Thus, CHANGED-VARS include both variables that
; actually contribute to why some measure goes down and variables like
; accumulators that are just along for the ride. UNCHANGEABLE-VARS is a list
; of all those vars which may not be changed by any substitution if this
; induction is to be sound for the reasons specified. TESTS-AND-ALISTS-LST
; is a list of TESTS-AND-ALISTS which indicates the case analysis for the
; induction and how the various induction hypotheses are obtained via
; substitutions. JUSTIFICATION is the JUSTIFICATION that justifies this
; induction, and INDUCTION-TERM is the term that suggested this induction and
; from which you obtain the actuals to substitute into the template.
; OTHER-TERMS are terms whose induction candidates have been merged into this
; one for heuristic reasons.
(GENERALIZE-LEMMA (NAME TERM) NIL)
; This record records a GENERALIZE lemma with name NAME. The TERM is just a
; well-formed formula, assumed to be a theorem of course, translated but
; possibly involving IMPLIES and the binary AND. These records are collected
; on the TYPE-NAME-AND-LEMMA-LST and used when a term, x, is generalized by
; scanning the list for all formulas involving x -- modulo a unification of
; course -- and adding to the hypothesis of the theorem, before it is
; generalized, the appropriately instantiated formulas found.
(JUSTIFICATION (SUBSET MEASURE-TERM RELATION LEMMAS) NIL)
; Consider the INDUCTION-MACHINE for some function. This record gives one
; justification for it. In particular, MEASURE-TERM, which is a term on a
; subset of the formals of the function, decreases according to the
; well-founded relation RELATION in each hypothesis of the INDUCTION-MACHINE.
; SUBSET is the measured subset of formals. The fact that the measure
; decreases can be proved using the lemmas in the list LEMMAS.
(LINEAR-LEMMA (NAME HYPS CONCL MAX-TERM) NIL)
; Internal form of a LINEAR lemma. NAME is the event name, HYPS is the list
; of hypotheses, and POLY is the LINEARIZEd conclusion.
(LINEAR-POT (VAR POSITIVES NEGATIVES) T)
(MEASURE-RULE (CONDITION-LIST THE-LESSER STRENGTH-SIGN THE-GREATER
INDUCTION-LEMMA-NAME MEASURE)
NIL)
; A record used to store the representation of an INDUCTION lemma. The
; MEASURE field contains the pair (C . R) where C is a measure function name
; and R is a well-founded relation name. The name of the lemma represented
; by the rule is stored in the INDUCTION-LEMMA-NAME field. The hypotheses of
; the lemma are in the CONDITION-LIST field. The form of the conclusion of
; the lemma depends on the contents of the STRENGTH-SIGN field. If that
; field contains a - (minus sign) then the conclusion is:
; (R (C . THE-LESSER) (C . THE-GREATER)),
; where THE-LESSER and THE-GREATER are the contents of the fields of those
; names. Otherwise, the STRENGTH-SIGN field contains a 0 and the conclusion
; is the disjunction of the one given above and the term:
; (EQUAL (C . THE-LESSER) (C . THE-GREATER)).
(POLY (CONSTANT ALIST ASSUMPTIONS LITERALS LEMMAS) T)
; CONSTANT is a FIXP. ALIST is an alist of pairs of the form (ti . ki) where
; ti is a term and ki is a FIXP. ASSUMPTIONS is a list of terms. LITERALS
; is a list of terms. LEMMAS is a list of lemma names, (LIST 'MARK)'s -- as
; constructed by ADD-TERMS-TO-POT-LST, or a term. A POLY represents an
; implication hyps -> concl, where hyps is the conjunction of ASSUMPTIONS and
; concl is CONSTANT + k1*t1 + ... + kn*tn <= 0, over the integers. Every
; POLY in SIMPLIFY-CLAUSE-POT-LST is being assumed. See ADD-TERMS-TO-POT-LST
; for more details about LITERALS and LEMMAS.
(REWRITE-RULE (NAME HYPS CONCL LOOP-STOPPER) NIL)
; These records are used to represent rewrite rules. The NAME field contains
; the name of the lemma or axiom. The HYPS is a list of terms whose
; conjunction is the hypothesis of the lemma. The CONCL is the term which is
; the conclusion of the lemma. The LOOP-STOPPER is an alist dotting vars to
; vars and used to prevent infinite rewrite loops due to permutative rewrite
; rules. The rewrite cannot be performed if the instantiation of the CDR of
; some pair is lexicographically bigger than or equal to -- see
; LOOP-STOPPER-GTE -- the instantiation of the CAR.
(TESTS-AND-ALISTS (TESTS ALISTS) NIL)
; A list of these records forms the TESTS-AND-ALISTS-LST component of a
; CANDIDATE record. The TESTS field contains a list of forms and the ALISTS
; field a list of alists. If the conjunction of the tests is true then some
; measure goes down on the n-tuples produced by each alist. The alist
; contains explicitly pairs of the form (v . v) if v is an unchanging
; controller. The soundness of MERGE-CANDS rests on this fact.
(TESTS-AND-CASE (TESTS CASE) NIL)
; This is like a TESTS-AND-CASES except that the CASE component contains
; exactly one case. A list of TESTS-AND-CASEs is a flattened machine.
(TESTS-AND-CASES (TESTS CASES) NIL)
; A list of these compose a machine (see INDUCTION-MACHINE) The TESTS field
; contains a list of terms whose conjunction must be true before the machine
; can "execute" the cases. The CASES field contains a list of arglists of
; the recursive calls governed by the the tests. By the nature of the
; machine, all TESTS are previously defined concepts and only the CASES
; involve the new function.
(TYPE-PRESCRIPTION-NAME-AND-PAIR (NAME PAIR) NIL)
; The TYPE-PRESCRIPTION-LST property is a list of these records. The NAME is
; the name of the rewrite lemma -- or definition -- that gave rise to the
; type prescription pair (ts . args) PAIR for the function under which this
; type prescription is hung.
(TYPE-RESTRICTION (TERM TYPE-SET DEFAULT)
NIL))))
; This record is used to represent processed type restrictions as found on
; the destructors of shells. The TERM component is a normalized term
; composed of recognizers applied to the variable X, possibly negated, and
; possibly disjoined or conjoined with binary OR or AND. The TYPE-SET
; component is the corresponding bit mask. The DEFAULT is the specified
; default object satisfying the type set. At prove time no one looks at
; TERM. It is examined during add shells and is used in the rewrite rules
; added.
(DEFCONST LEMMA-STACK (PROGN (CREATE-LEMMA-STACK 10) LEMMA-STACK))
(DEFCONST LINEARIZE-ASSUMPTIONS-STACK
(PROGN (CREATE-LINEARIZE-ASSUMPTIONS-STACK 10) LINEARIZE-ASSUMPTIONS-STACK))